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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cf93a66cfb..a1e8f9bd1d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1257,7 +1257,9 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma in let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in let evdc = - catch_error trace (understand_ltac expand_evar sigma env vars kind) c in + catch_error trace + (understand_ltac ~resolve_classes:use_classes expand_evar sigma env vars kind) c + in let (evd,c) = if expand_evar then solve_remaining_evars fail_evar use_classes @@ -1279,8 +1281,8 @@ let interp_type = interp_constr_gen IsType let interp_open_constr_gen kind ist = interp_gen kind ist false true false false -let interp_open_constr ccl = - interp_open_constr_gen (OfType ccl) +let interp_open_constr ccl ist = + interp_gen (OfType ccl) ist false true false (ccl<>None) let interp_pure_open_constr ist = interp_gen (OfType None) ist false false false false |