From 3c3bbccb00cb1c13c28a052488fc2c5311d47298 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 24 Dec 2009 01:00:25 +0000
Subject: 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
---
 proofs/evar_refiner.ml  | 2 +-
 proofs/tacexpr.ml       | 6 +++---
 proofs/tactic_debug.mli | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'proofs')

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 :
-- 
cgit v1.2.3