Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,

fix the type of the term which has to be in the signature of the evar
to declare); some problems remain though (see next commit).

1 files changed, 12 insertions, 8 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8f696b84c..aaf6e2a3d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Pp
 open Errors
 open Names
 open Term
@@ -466,10 +467,8 @@ let make_projectable_subst aliases sigma evi args =
  * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
  *)
 
-let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
-  let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
-  let evd,ty_t_in_env = refresh_universes false evd ty_t_in_env in
-  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
+let define_evar_from_virtual_equation define_fun env evd t_in_env ty_t_in_sign sign filter inst_in_env =
+  let evd,evar_in_env = new_evar_instance sign evd ty_t_in_sign ~filter inst_in_env in
   let t_in_env = whd_evar evd t_in_env in
   let evd = define_fun env evd None (destEvar evar_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
@@ -505,13 +504,16 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
     List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
       let id = next_name_away na avoid in
       let evd,t_in_sign =
-        define_evar_from_virtual_equation define_fun env evd t_in_env
-          sign filter inst_in_env in
+        let s = Retyping.get_sort_of env evd t_in_env in
+        let evd,ty_t_in_sign = refresh_universes false evd (mkSort s) in
+        define_evar_from_virtual_equation define_fun env evd t_in_env 
+          ty_t_in_sign sign filter inst_in_env in
       let evd,b_in_sign = match b with
       | None -> evd,None
       | Some b ->
+  Printf.printf "!!%!";
           let evd,b = define_evar_from_virtual_equation define_fun env evd b
-            sign filter inst_in_env in
+            t_in_sign sign filter inst_in_env in
           evd,Some b in
       (push_named_context_val (id,b_in_sign,t_in_sign) sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
@@ -521,8 +523,10 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
   in
   let evd,ev2ty_in_sign =
+    let s = Retyping.get_sort_of env evd ty_in_env in
+    let evd,ty_t_in_sign = refresh_universes false evd (mkSort s) in
     define_evar_from_virtual_equation define_fun env evd ty_in_env
-      sign2 filter2 inst2_in_env in
+      ty_t_in_sign sign2 filter2 inst2_in_env in
   let evd,ev2_in_sign =
     new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
   let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in