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

2 files changed, 10 insertions, 10 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 1fde7b245a..fe7038d3a3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -246,10 +246,10 @@ let rec pr_generic prc prlc prtac x =
       pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x)
   | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
   | ConstrWithBindingsArgType ->
-      let (c,b) = out_gen wit_constr_with_bindings x in
-      pr_with_bindings prc prlc (c,out_bindings b)
+      let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in
+      pr_with_bindings prc prlc (c,b)
   | BindingsArgType ->
-      pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x))
+      pr_bindings_no_with prc prlc (out_gen wit_bindings x).Evd.it
   | List0ArgType _ ->
       hov 0 (pr_sequence (pr_generic prc prlc prtac)
 	(fold_list0 (fun a l -> a::l) x []))
@@ -288,7 +288,7 @@ let pr_raw_extend prc prlc prtac =
 let pr_glob_extend prc prlc prtac =
   pr_extend_gen (pr_glob_generic prc prlc prtac)
 let pr_extend prc prlc prtac =
-  pr_extend_gen (pr_generic (fun c -> prc (Evd.empty,c)) (fun c -> prlc (Evd.empty,c)) prtac)
+  pr_extend_gen (pr_generic prc prlc prtac)
 
 (**********************************************************************)
 (* The tactic printer                                                 *)
@@ -1008,12 +1008,12 @@ let strip_prod_binders_rawterm n (ty,_) =
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
-let strip_prod_binders_constr n (sigma,ty) =
+let strip_prod_binders_constr n ty =
   let rec strip_ty acc n ty =
-    if n=0 then (List.rev acc, (sigma,ty)) else
+    if n=0 then (List.rev acc, ty) else
       match Term.kind_of_term ty with
           Term.Prod(na,a,b) ->
-            strip_ty (([dummy_loc,na],(sigma,a))::acc) (n-1) b
+            strip_ty (([dummy_loc,na],a)::acc) (n-1) b
         | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
@@ -1059,8 +1059,8 @@ and pr_glob_match_rule env t =
 
 let typed_printers =
     (pr_glob_tactic_level,
-     pr_open_constr_env,
-     pr_open_lconstr_env,
+     pr_constr_env,
+     pr_lconstr_env,
      pr_lconstr_pattern,
      pr_evaluable_reference_env,
      pr_inductive,
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 7fa33119d6..f84a2deb27 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -74,7 +74,7 @@ val pr_glob_extend:
     string -> glob_generic_argument list -> std_ppcmds
 
 val pr_extend :
-  (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) ->
+  (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
   (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
     string -> typed_generic_argument list -> std_ppcmds