convertibility was taking a metasenv but not using it

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index e867b74934e4c51a52ad1c79a30bc620040d667a..38982d799768183d7353f1d205cfe2236000a699 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -91,7 +91,7 @@ let get_checked_def = function
 ;;
 
 let get_checked_indtys = function
-  | NReference.Ref (_, uri, (NReference.Ind n|NReference.Con (n,_))) ->
+  | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
       (match get_checked_obj uri with
       | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
         inductive,leftno,tys,att,n