get_checked_indtys can take a constructor reference

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index cca0e5cdf55868a9e38c411710f0a51e3295afa4..1e2cd913e8074a70226b3b067f20840ba6a7ba35 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -56,7 +56,7 @@ let get_checked_def = function
 ;;
 
 let get_checked_indtys = function
-  | NReference.Ref (_, uri, NReference.Ind 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