diff options
| author | msozeau | 2012-03-14 13:33:09 +0000 |
|---|---|---|
| committer | msozeau | 2012-03-14 13:33:09 +0000 |
| commit | 9f7450858ae9ad3360180fada06e1350680d53e1 (patch) | |
| tree | d45879840f2bfe7db74a876e5c140025e61ddf96 /pretyping | |
| parent | a4c0ec668652bf8d9e288fddb88901e272779960 (diff) | |
Revise API of understand_ltac to be parameterized by a flag for resolution of evars.
Used when interpreting a constr in Ltac: resolution is now launched if the constr
is casted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 2 |
3 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9d62eeb131..0f77053179 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -67,7 +67,7 @@ let error_needs_inversion env x t = module type S = sig val compile_cases : - loc -> case_style -> + loc -> case_style -> (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> glob_constr option * tomatch_tuples * cases_clauses -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1d5c4d47f4..08eaa88673 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -138,6 +138,7 @@ let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) = (* Side-effect *) !evdref,c +<<<<<<< HEAD (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false @@ -736,8 +737,8 @@ let understand sigma env ?expected_type:exptyp c = let understand_type sigma env c = snd (ise_pretype_gen true true true sigma env ([],[]) IsType c) -let understand_ltac expand_evar sigma env lvar kind c = - ise_pretype_gen expand_evar false false sigma env lvar kind c +let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c = + ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 34bafdb23c..75e507afdd 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -59,7 +59,7 @@ val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> constraint : tell if interpreted as a possibly constrained term or a type *) -val understand_ltac : +val understand_ltac : ?resolve_classes:bool -> bool -> evar_map -> env -> ltac_var_map -> typing_constraint -> glob_constr -> pure_open_constr |