aded a prototype of chtting aboit tacticals

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 03acb40cb7b7b3c59958b8706a2273b528140bd3..e4532d913bf77d69027eda8420bb9e65cdd1c7ca 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -152,7 +152,6 @@ let exp_impl metasenv subst context term =
         in
         let funs' = combine (funs, types) in
         metasenv', Cic.CoFix (i, funs')
-    | term -> metasenv,term
   and do_subst metasenv context subst =
     List.fold_right
       (fun (uri, term) (metasenv, substs) ->
@@ -361,14 +360,11 @@ and type_of_aux' metasenv context t ugraph =
             let te',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context te ugraph1
             in
-              (try
                  let subst''',metasenv''',ugraph3 =
                    fo_unif_subst subst'' context metasenv'' 
-                     inferredty ty ugraph2
+                     inferredty ty' ugraph2
                  in
                    C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
-               with
-               | _ -> raise (RefineFailure (lazy "Cast")))
         | C.Prod (name,s,t) ->
             let carr t subst context = CicMetaSubst.apply_subst subst t in
             let coerce_to_sort 
@@ -481,7 +477,7 @@ and type_of_aux' metasenv context t ugraph =
                 ) tl ([],subst',metasenv',ugraph1)
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
-              eat_prods subst'' metasenv'' context 
+              eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
@@ -744,6 +740,22 @@ and type_of_aux' metasenv context t ugraph =
                         (Cic.Appl (outtype::right_args@[term']))),
                      subst,metasenv,ugraph)
            | _ ->    (* easy case *)
+             let outtype,outtypety, subst, metasenv,ugraph4 =
+               type_of_aux subst metasenv context outtype ugraph4
+             in
+             let tlbody_and_type,subst,metasenv,ugraph4 =
+               List.fold_right
+                 (fun x (res,subst,metasenv,ugraph) ->
+                    let x',ty,subst',metasenv',ugraph1 =
+                      type_of_aux subst metasenv context x ugraph
+                    in
+                      (x', ty)::res,subst',metasenv',ugraph1
+                 ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+             in
+             let _,_,subst,metasenv,ugraph4 =
+               eat_prods false subst metasenv context 
+                 outtypety tlbody_and_type ugraph4
+             in
              let _,_, subst, metasenv,ugraph5 =
                type_of_aux subst metasenv context
                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
@@ -1001,7 +1013,9 @@ and type_of_aux' metasenv context t ugraph =
                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
                 (CicPp.ppterm t2''))))
 
-  and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
+  and eat_prods 
+    allow_coercions subst metasenv context hetype tlbody_and_type ugraph 
+  =
     let rec mk_prod metasenv context =
       function
           [] ->
@@ -1068,7 +1082,7 @@ and type_of_aux' metasenv context t ugraph =
                          fo_unif_subst subst context metasenv hety s ugraph
                        in
                          hete,subst,metasenv,ugraph1
-                     with exn ->
+                     with exn when allow_coercions ->
                        (* we search a coercion from hety to s *)
                        let coer = 
                          let carr t subst context =