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 --- plugins/quote/quote.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/quote') 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 -- cgit v1.2.3