Bug fixed: an unrefined term was passed around while checking explicit named

substitutions.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index ccf662f185967f799faacbcb4fabf914adc005db..2b4b68947b9ca8025edf0dd174761b5cb6ca4db1 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -849,9 +849,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
       match tl with
           [] -> [],metasubst,metasenv,ugraph
-        | ((uri,t) as subst)::tl ->
+        | (uri,t)::tl ->
             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
             let typeofvar =
+prerr_endline ("<<<" ^ CicPp.ppterm ty_uri);
               CicSubstitution.subst_vars substs ty_uri in
               (* CSC: why was this code here? it is wrong
                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
@@ -867,8 +868,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                  ) ;
               *)
             let t',typeoft,metasubst',metasenv',ugraph2 =
-              type_of_aux metasubst metasenv context t ugraph1
-            in
+              type_of_aux metasubst metasenv context t ugraph1 in
+            let subst = uri,t' in
             let metasubst'',metasenv'',ugraph3 =
               try
                 fo_unif_subst