Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 57f99b52b405c48f1f26c8de6483046778ef1292..11b58895ea384ace50665652ff28f60c61e2fe32 100644 (file)
--- 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