]> matita.cs.unibo.it Git - helm.git/commitdiff
get_checked_indtys can take a constructor reference
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 May 2008 16:43:04 +0000 (16:43 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 5 May 2008 16:43:04 +0000 (16:43 +0000)
helm/software/components/ng_kernel/nCicEnvironment.ml

index cca0e5cdf55868a9e38c411710f0a51e3295afa4..1e2cd913e8074a70226b3b067f20840ba6a7ba35 100644 (file)
@@ -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