From 016e4c6fc449b50ac19e73eb952cfb2dc64f4398 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Jul 2005 10:21:29 +0000
Subject: [PATCH] Bug fixed: metavariables generated by the saturation in the
 rewrite tactic were not declared as new goals in the output of the tactic.

---
 helm/matita/tests/rewrite.ma          | 13 ++++++++++++-
 helm/ocaml/tactics/equalityTactics.ml | 21 ++++++++++++++-------
 2 files changed, 26 insertions(+), 8 deletions(-)

diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index 3941ab0cb..aa4fa1f32 100644
--- a/helm/matita/tests/rewrite.ma
+++ b/helm/matita/tests/rewrite.ma
@@ -4,7 +4,7 @@ alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "leibnitz's equality". 
 alias symbol "plus" (instance 0) = "natural plus".
-
+alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
 
 theorem a:
   \forall a,b:nat.
@@ -21,3 +21,14 @@ simplify.
 reflexivity.
 qed.
  
+theorem t: \forall n. 0=0 \to n = n + 0.
+ intros.
+ apply plus_n_O.
+qed.
+
+(* In this test "rewrite < t" should open a new goal 0=0 and put it in *)
+(* the goallist so that the THEN tactical closes it using reflexivity. *)
+theorem foo: \forall n. n = n + 0.
+ intros.
+ rewrite < t; reflexivity.
+qed.
\ No newline at end of file
diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 4a6c445e6..7eae7fb5c 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -45,7 +45,7 @@ let rewrite_tac ~direction ~pattern equality =
   let ty_eq,ugraph = 
     CicTypeChecker.type_of_aux' metasenv context equality 
       CicUniv.empty_ugraph in 
-  let (ty_eq,metasenv,arguments,fresh_meta) =
+  let (ty_eq,metasenv',arguments,fresh_meta) =
    ProofEngineHelpers.saturate_term
     (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq in
   let equality =
@@ -66,16 +66,17 @@ let rewrite_tac ~direction ~pattern equality =
   (* now we always do as if direction was `LeftToRight *)
   let fresh_name = 
     FreshNamesGenerator.mk_fresh_name 
-    ~subst:[] metasenv context C.Anonymous ~typ:ty in
+    ~subst:[] metasenv' context C.Anonymous ~typ:ty in
   let lifted_t1 = CicSubstitution.lift 1 t1 in
   let lifted_gty = CicSubstitution.lift 1 gty in
   let lifted_conjecture =
     metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
   let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in
-  let subst,metasenv,ugraph,_,selected_terms_with_context =
+  let subst,metasenv',ugraph,_,selected_terms_with_context =
    ProofEngineHelpers.select
-    ~metasenv ~ugraph ~conjecture:lifted_conjecture ~pattern:lifted_pattern in
-  let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+    ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture
+     ~pattern:lifted_pattern in
+  let metasenv' = CicMetaSubst.apply_subst_metasenv subst metasenv' in
   let what,with_what = 
    (* Note: Rel 1 does not live in the context context_of_t           *)
    (* The replace_lifting_csc_0 function will take care of lifting it *)
@@ -92,7 +93,7 @@ let rewrite_tac ~direction ~pattern equality =
   let equality = CicMetaSubst.apply_subst subst equality in
   let gty' = CicSubstitution.subst t2 abstr_gty in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let metasenv' = (fresh_meta,context,gty')::metasenv in
+  let metasenv' = (fresh_meta,context,gty')::metasenv' in
   let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   let exact_proof = 
     C.Appl [eq_ind ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]
@@ -102,7 +103,13 @@ let rewrite_tac ~direction ~pattern equality =
       (PT.exact_tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
   in
   assert (List.length goals = 0) ;
-  (proof',[fresh_meta])
+  let goals = List.map (fun (i,_,_) -> i) metasenv' in
+  let goals =
+   List.filter
+    (fun i ->
+      not (List.exists (fun (j,_,_) -> i=j) metasenv)) goals
+  in
+   (proof',goals)
  in
   ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
   
-- 
2.39.2