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, 14 insertions, 13 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 16cc3a7316..e1a16ce498 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -215,9 +215,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (array_last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (pattern_of_constr f, Array.map aux args)
+          PApp (pattern_of_constr Evd.empty f, Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pattern_of_constr c
+      | _ -> pattern_of_constr Evd.empty c
   in
   aux bodyi
 
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 7d1f2cd62e..f909f9e0a9 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -569,7 +569,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  error_unexpected_type_loc
                     (loc_of_rawconstr c) env ( !evdref) tj.utj_val v
 
-  let pretype_gen fail_evar resolve_classes evdref env lvar kind c =
+  let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
     let c' = match kind with
       | OfType exptyp ->
 	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
@@ -581,7 +581,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       evdref :=
         Typeclasses.resolve_typeclasses ~onlyargs:false
 	  ~split:true ~fail:fail_evar env !evdref;
-    let c = nf_evar !evdref c' in
+    let c = if expand_evar then nf_evar !evdref c' else c' in
     if fail_evar then check_evars env Evd.empty !evdref c;
     c
 
@@ -606,30 +606,30 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
      fail on unresolved evars; the unsafe_judgment list allows us to
      extend env with some bindings *)
 
-  let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c =
+  let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
-    let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in
+    let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
   let understand_gen kind sigma env c =
-    snd (ise_pretype_gen true true sigma env ([],[]) kind c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
 
   let understand sigma env ?expected_type:exptyp c =
-    snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c)
+    snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
 
   let understand_type sigma env c =
-    snd (ise_pretype_gen false true sigma env ([],[]) IsType c)
+    snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)
 
-  let understand_ltac sigma env lvar kind c =
-    ise_pretype_gen false true sigma env lvar kind c
+  let understand_ltac expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false true sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-    ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c
+    ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
 
   let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-    pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c
+    pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
 end
 
 module Default : S = SubtacPretyping_F(Coercion.Default)
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 476724ba6d..32a1755ca0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -189,6 +189,7 @@ let string_of_hole_kind = function
   | TomatchTypeParameter _ -> "TomatchTypeParameter"
   | GoalEvar -> "GoalEvar"
   | ImpossibleCase -> "ImpossibleCase"
+  | MatchingVar _ -> "MatchingVar"
 
 let evars_of_term evc init c =
   let rec evrec acc c =