From 7d6f47c980081e06fee46c08d5b5bd7faf1e6aa9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 May 2008 16:43:04 +0000 Subject: [PATCH] get_checked_indtys can take a constructor reference --- helm/software/components/ng_kernel/nCicEnvironment.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index cca0e5cdf..1e2cd913e 100644 --- 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 -- 2.39.2