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

1 files changed, 3 insertions, 3 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e7bca648c..bc2953408 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,