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

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 16cc3a731..e1a16ce49 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