Bug fixed: metavariables generated by the saturation in the rewrite tactic

were not declared as new goals in the output of the tactic.

diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma
index 3941ab0cb4d1e1d53cbc0be4b6fc64a921864714..aa4fa1f3285ad09f7cb64ce287cda697680b3881 100644 (file)
--- 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 4a6c445e6e359702300d291c246bb6c30b89b3ef..7eae7fb5c0ee402d0761dd39df7fe4050d7ad4ce 100644 (file)
--- 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)