Merge PR#379: Introducing evar-insensitive constrs

1 files changed, 4 insertions, 2 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1248b60a76..fb0c22c2b7 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,8 @@ let extend_with_ref_list l seq gl =
   let l = expand_constructor_hints l in
   let f gr (seq,gl) =
     let gl, c = pf_eapply Evd.fresh_global gl gr in
-    let typ=(pf_unsafe_type_of gl c) in
+    let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
+    let typ = EConstr.Unsafe.to_constr typ in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -214,8 +215,9 @@ let extend_with_auto_hints l seq gl=
       | Res_pf_THEN_trivial_fail (c,_) ->
           let (c, _, _) = c in
 	  (try
-	     let gr = global_of_constr c in
+	     let (gr, _) = Termops.global_of_constr (project gl) c in
 	     let typ=(pf_unsafe_type_of gl c) in
+	     let typ = EConstr.Unsafe.to_constr typ in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in