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, 2 insertions, 2 deletions

diff --git a/interp/genarg.mli b/interp/genarg.mli
index ef7c3e864e..664ed43f06 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -195,11 +195,11 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
 
 val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
 val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type
-val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type
+val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type
 
 val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
 val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
-val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type
+val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type
 
 val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type
 val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type