diff options
| author | msozeau | 2008-10-25 15:02:34 +0000 |
|---|---|---|
| committer | msozeau | 2008-10-25 15:02:34 +0000 |
| commit | 47eb59cfa5baf2e67410ba00a0d2b7f32ce80e94 (patch) | |
| tree | 612c352e2d45d1b4ddb6d0c0373ab3d7c89fe08c /tactics/tacinterp.ml | |
| parent | ca3131d423dd32a8b02a2ca5eb9074dff2cae1b7 (diff) | |
More debugging of handling of open constrs with typeclasses:
avoid trying to resolve classes early in open constr arguments for Ltac,
the tactics themselves should do whatever's appropriate with the constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11503 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index aa5aaed3b7..063f387ac3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1438,7 +1438,7 @@ let solve_remaining_evars env initial_sigma evd c = Pretype_errors.error_unsolvable_implicit loc env sigma evi src None) | _ -> map_constr proc_rec c in - proc_rec c + proc_rec (Evarutil.nf_isevar !evdref c) let interp_gen kind ist sigma env (c,ce) = let (ltacvars,unbndltacvars as vars) = constr_list ist env in @@ -1466,6 +1466,10 @@ let interp_open_constr ccl ist sigma env cc = let evd,c = interp_gen (OfType ccl) ist sigma env cc in (evars_of evd,c) +let interp_open_type ccl ist sigma env cc = + let evd,c = interp_gen IsType ist sigma env cc in + (evars_of evd,c) + let interp_constr = interp_econstr (OfType None) let interp_type = interp_econstr IsType @@ -2200,7 +2204,7 @@ and interp_atomic ist gl = function h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l) | TacCut c -> h_cut (pf_interp_type ist gl c) | TacAssert (t,ipat,c) -> - let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in + let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in abstract_tactic (TacAssert (t,ipat,inj_open c)) (Tactics.forward (Option.map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) |