From 33a4938d5ce3a5c240c0d35b6362c8072f8ba482 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 14:35:57 +0000 Subject: [PATCH] Axioms were not indexed. From: sacerdot --- helm/software/components/ng_tactics/nnAuto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 57f99b52b..11b58895e 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -74,7 +74,7 @@ let is_a_fact status ty = branch status ty = 0 let is_a_fact_obj s uri = let obj = NCicEnvironment.get_checked_obj uri in match obj with - | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) -> + | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) -> is_a_fact s (mk_cic_term [] ty) (* aggiungere i costruttori *) | _ -> false -- 2.39.2