From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 24 Mar 2010 14:35:57 +0000 (+0000)
Subject: Axioms were not indexed.
X-Git-Tag: make_still_working~2971
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33a4938d5ce3a5c240c0d35b6362c8072f8ba482;p=helm.git

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 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