Wish of Maggesi implemented: the type of the morphism compatibility lemma

is now the one that is shown to the user (and not only convertible to it).
In this way it is possible to register the lemma in the Hint database.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 17 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 315e9991d..4e17fef9e 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -168,10 +168,10 @@ let coq_equality_morphism_of_setoid_theory =
  lazy(constant ["Setoid"] "equality_morphism_of_setoid_theory")
 let coq_make_compatibility_goal =
  lazy(constant ["Setoid"] "make_compatibility_goal")
-let coq_make_compatibility_goal_ref =
- lazy(reference ["Setoid"] "make_compatibility_goal")
-let coq_make_compatibility_goal_aux_ref =
- lazy(reference ["Setoid"] "make_compatibility_goal_aux")
+let coq_make_compatibility_goal_eval_ref =
+ lazy(eval_reference ["Setoid"] "make_compatibility_goal")
+let coq_make_compatibility_goal_aux_eval_ref =
+ lazy(eval_reference ["Setoid"] "make_compatibility_goal_aux")
 
 let coq_App = lazy(constant ["Setoid"] "App")
 let coq_ToReplace = lazy(constant ["Setoid"] "ToReplace")
@@ -784,8 +784,7 @@ let new_morphism m signature id hook =
          let find_relation_class t real_t =
           try
            let rel = find_relation_class t in
-            rel,
-             unify_relation_class_carrier_with_type (Global.env ()) rel real_t
+            rel, unify_relation_class_carrier_with_type env rel real_t
           with Not_found ->
            errorlabstrm "Add Morphism"
             (str "Not a valid signature: " ++ prterm t ++
@@ -834,20 +833,22 @@ let new_morphism m signature id hook =
      begin
       new_edited id
        (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
-      Pfedit.start_proof id (IsGlobal (Proof Lemma)) 
-       (Declare.clear_proofs (Global.named_context ()))
-       lem hook;
       (* "unfold make_compatibility_goal" *)
-      Pfedit.by
-       (Tactics.unfold_constr
-        (Lazy.force coq_make_compatibility_goal_ref)) ;
+      let lem =
+       Reductionops.clos_norm_flags
+        (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref))
+        env Evd.empty lem in
       (* "unfold make_compatibility_goal_aux" *)
-      Pfedit.by
-       (Tactics.unfold_constr
-        (Lazy.force coq_make_compatibility_goal_aux_ref)) ;
+      let lem =
+       Reductionops.clos_norm_flags
+        (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
+        env Evd.empty lem in
       (* "simpl" *)
-      Pfedit.by Tactics.simpl_in_concl ;
-      Options.if_verbose msg (Printer.pr_open_subgoals ());
+      let lem = Tacred.nf env Evd.empty lem in
+       Pfedit.start_proof id (IsGlobal (Proof Lemma)) 
+        (Declare.clear_proofs (Global.named_context ()))
+        lem hook;
+       Options.if_verbose msg (Printer.pr_open_subgoals ());
      end
 
 let morphism_hook _ ref =