X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=c3e2b6b4894929dc84648e5549a3c7be412bf6f2;hb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;hp=fabfcf4de2c961dbdb57e0cb81fb4f0b2006401c;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index fabfcf4de..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 -> 
@@ -750,10 +747,11 @@ let split_goals_with_metas metasenv subst gl =
 let order_new_goals metasenv subst open_goals ppterm =
   let prop,rest = split_goals_in_prop metasenv subst open_goals in
   let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
+  let closed_type, open_type = split_goals_with_metas metasenv subst rest in
   let open_goals =
-    (List.map (fun x -> x,P) (closed_prop @ open_prop)) 
+    (List.map (fun x -> x,P) (open_prop @ closed_prop)) 
     @ 
-    (List.map (fun x -> x,T) rest)
+    (List.map (fun x -> x,T) (open_type @ closed_type))
   in
   let tys = 
     List.map