From 32e3ed47b676960383d53961492374526189161d Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 15 Oct 2004 13:10:39 +0000
Subject: 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
---
 tactics/setoid_replace.ml | 35 ++++++++++++++++++-----------------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 315e9991d7..4e17fef9ed 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 =
-- 
cgit v1.2.3