X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=c3e2b6b4894929dc84648e5549a3c7be412bf6f2;hb=27bce1d83422883b6415862ec92e75baf4f87186;hp=37f0939bd16e447e48d6420514ed5537b8d26c1f;hpb=78ab40460460f98d294365543659fe3cafe7503d;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 37f0939bd..c3e2b6b48 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -30,6 +30,14 @@ let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
+let is_propositional context sort = 
+  match CicReduction.whd context sort with
+  | Cic.Sort Cic.Prop 
+  | Cic.Sort (Cic.CProp _) -> true
+  | _-> false
+;;
+
+
 type auto_params = Cic.term list * (string * string) list 
 
 let elems = ref [] ;;
@@ -133,11 +141,7 @@ let is_unit_equation context metasenv oldnewmeta term =
             CicTypeChecker.type_of_aux' metasenv context mt 
               CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -314,11 +318,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u
             CicTypeChecker.type_of_aux' metasenv context mt 
               CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -686,7 +686,7 @@ let ppterm ctx t =
 ;;
 let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
-  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+  is_propositional context sort
 ;;
 
 let assert_proof_is_valid proof metasenv context goalty =
@@ -723,10 +723,7 @@ let split_goals_in_prop metasenv subst gl =
       let _,context,ty = CicUtil.lookup_meta g metasenv in
       try
         let sort,u = typeof ~subst metasenv context ty ugraph in
-        let b,_ = 
-          CicReduction.are_convertible 
-            ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
-        b
+        is_propositional context sort
       with 
       | CicTypeChecker.AssertFailure s 
       | CicTypeChecker.TypeCheckerFailure s ->