Opened the possibility to type Ltac patterns but it is not fully functional yet

- to type patterns w/o losing the information of what subterm is a hole
  would need to remember where holes were in "understand", but "understand"
  needs sometimes to instantiate evars to ensure the type of an evar
  is not its original type but the type of its instance (what can
  e.g. lower a universe level); we would need here to update evars
  type at the same time we define them but this would need in turn to
  check the convertibility of the actual and expected type since otherwise
  type-checking constraints may disappear;
- typing pattern is apparently expensive in time; is it worth to do it
  for the benefit of pattern-matching compilation and coercion insertion?

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

3 files changed, 6 insertions, 6 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b3976704af..e4fab3f2f8 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     error "Instantiate called on already-defined evar";
   let env = Evd.evar_env evi in
   let sigma',typed_c =
-    try Pretyping.Default.understand_ltac sigma env ltac_var
+    try Pretyping.Default.understand_ltac true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1d4766494d..04b7a225c7 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -273,7 +273,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
 (* Globalized tactics *)
 and glob_tactic_expr =
     (rawconstr_and_expr,
-     constr_pattern,
+     rawconstr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -317,7 +317,7 @@ type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen
 
 type glob_atomic_tactic_expr =
     (rawconstr_and_expr,
-     constr_pattern,
+     rawconstr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
@@ -327,7 +327,7 @@ type glob_atomic_tactic_expr =
 
 type glob_tactic_arg =
     (rawconstr_and_expr,
-     constr_pattern,
+     rawconstr_and_expr * constr_pattern,
      evaluable_global_reference and_short_name or_var,
      inductive or_var,
      ltac_constant located or_var,
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index ab59f208af..0a5e6087b1 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -24,7 +24,7 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit
 val set_match_pattern_printer :
   (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
 val set_match_rule_printer :
-  ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
+  ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
     unit
 
 (* Debug information *)
@@ -41,7 +41,7 @@ val db_constr : debug_info -> env -> constr -> unit
 
 (* Prints the pattern rule *)
 val db_pattern_rule :
-  debug_info -> int -> (constr_pattern,glob_tactic_expr) match_rule -> unit
+  debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
 
 (* Prints a matched hypothesis *)
 val db_matched_hyp :