Generic support for open terms in tactics

We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
  the general sigma of the goal so that tactics have no such low-level
  tclEVARS, Evd.merge, or check_evars to do:
  - what takes tclEVARS and check_evars in charge is now a new
    tactical of name tclWITHHOLES (this tactical has a flag to support
    tactics in either the "e"- mode and the non "e"- mode);
  - the merge of goal evars and holes is now done generically at
    interpretation time (in tacinterp) and as a side-effect it also
    anticipates the possibility to refer to evars of the goal in the
    arguments;
  - with this approach, we don't need such constr/open_constr or
    bindings/ebindings variants and we can get rid of all ugly
    inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
  this is the case e.g. of "rewrite !c" which morally reevaluates c at
  each new rewriting step; this kind of tactics still receive a
  specific sigma around their arguments and they have to merge evars
  and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.




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

4 files changed, 12 insertions, 6 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ff7cf5acc3..9bc818e861 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -78,6 +78,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
 	clenv.env clenv.evd
     else clenv.evd
   in
+  let clenv = { clenv with evd = evd' } in
   tclTHEN
     (tclEVARS evd')
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e7bca648c8..bc29534081 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -74,7 +74,7 @@ and tactic_expr =
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -85,7 +85,7 @@ and atomic_tactic_expr =
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5fa4a44ef7..b5c4a234d1 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -109,7 +109,7 @@ and tactic_expr =
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -120,7 +120,7 @@ and atomic_tactic_expr =
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (open_constr,
+  (constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index ff902d880b..e853c12b7c 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -185,6 +185,11 @@ val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
 val tactic_list_tactic : tactic_list -> tactic
 val goal_goal_list     : 'a sigma -> 'a list sigma
 
+(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
+   may have unresolved holes; if [solve_holes] these holes must be
+   resolved after application of the tactic; [sigma] must be an
+   extension of the sigma of the goal *)
+val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic
 
 (*s Functions for handling the state of the proof editor. *)