diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 16:06:47 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 16:06:47 +0200 |
commit | 4ad6dbef69f9fd4cb1b55efc252d67325068e6b1 (patch) | |
tree | 0c2c1f2310cf5751a2f97f29a0bfd5a8295d1da2 | |
parent | 48d56f49b1db47f393ef3e0f31d1b22adf497afa (diff) | |
parent | 5c5f7c8d6a6ed8cbb99b12dde09fdbcc30ca8ab9 (diff) |
Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings
-rw-r--r-- | CHANGES | 4 | ||||
-rw-r--r-- | dev/doc/changes.txt | 6 | ||||
-rw-r--r-- | interp/stdarg.ml | 2 | ||||
-rw-r--r-- | interp/stdarg.mli | 5 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 18 | ||||
-rw-r--r-- | tactics/tactics.ml | 3 | ||||
-rw-r--r-- | test-suite/bugs/closed/5153.v | 8 | ||||
-rw-r--r-- | test-suite/success/specialize.v | 8 |
8 files changed, 46 insertions, 8 deletions
@@ -22,6 +22,10 @@ Tactics beta-iota-reduced after type-checking. This has an impact on the type of the variables that the tactic "refine" introduces in the context, producing types a priori closer to the expectations. +- In "Tactic Notation" or "TACTIC EXTEND", entry "constr_with_bindings" + now uses type classes and rejects terms with unresolved holes, like + entry "constr" does. To get the former behavior use + "open_constr_with_bindings" (possible source of incompatibility. Vernacular Commands diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a2ae8254d..d52c18462 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -150,6 +150,12 @@ alternative solution would be to fully qualify Ltac modules, e.g. turning any call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not work for EXTEND macros though. +** Additional changes in tactic extensions ** + +Entry "constr_with_bindings" has been renamed into +"open_constr_with_bindings". New entry "constr_with_bindings" now +uses type classes and rejects terms with unresolved holes. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 34fc5b2dc..a393dd71c 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -59,6 +59,8 @@ let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" let wit_constr_with_bindings = make0 "constr_with_bindings" +let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" + let wit_bindings = make0 "bindings" let wit_red_expr = make0 "redexpr" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 6a98ee64d..be876504e 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -59,6 +59,11 @@ val wit_constr_with_bindings : glob_constr_and_expr with_bindings, constr with_bindings delayed_open) genarg_type +val wit_open_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8ed65c5d9..a9ec779d1 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -996,7 +996,7 @@ let interp_bindings ist env sigma = function let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr ist env sigma c in + let sigma, c = interp_constr ist env sigma c in sigma, (c,bl) let interp_open_constr_with_bindings ist env sigma (c,bl) = @@ -1025,7 +1025,7 @@ let interp_destruction_arg ist gl arg = | keep,ElimOnConstr c -> keep,ElimOnConstr { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_constr_with_bindings ist env sigma c in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) } | keep,ElimOnAnonHyp n as x -> x @@ -1678,8 +1678,8 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let sigma, cb = interp_constr_with_bindings ist env sigma cb in - let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac @@ -1690,7 +1690,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in let named_tac = let tac = Tactics.general_case_analysis ev keep cb in name_atomic ~env (TacCase(ev,(keep,cb))) tac @@ -1807,7 +1807,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let l,lp = List.split l in let sigma,el = - Option.fold_map (interp_constr_with_bindings ist env) sigma el in + Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in let tac = name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) (Tactics.induction_destruct isrec ev (l,el)) @@ -2044,6 +2044,11 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm Sigma.Unsafe.of_pair (c, sigma) } +let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> + let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in + Sigma.Unsafe.of_pair (c, sigma) + } + let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) end } @@ -2066,6 +2071,7 @@ let () = register_interp0 wit_open_constr (lifts interp_open_constr); register_interp0 wit_bindings interp_bindings'; register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; + register_interp0 wit_open_constr_with_bindings interp_open_constr_with_bindings'; register_interp0 wit_destruction_arg interp_destruction_arg'; () diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1975eed9d..c713a31fa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2959,8 +2959,7 @@ let specialize (c,lbind) ipat = let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in let sigma, term = if lbind == NoBindings then - let sigma = Typeclasses.resolve_typeclasses env sigma in - sigma, nf_evar sigma c + sigma, c else let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in diff --git a/test-suite/bugs/closed/5153.v b/test-suite/bugs/closed/5153.v new file mode 100644 index 000000000..be6407b5f --- /dev/null +++ b/test-suite/bugs/closed/5153.v @@ -0,0 +1,8 @@ +(* An example where it does not hurt having more type-classes resolution *) +Class some_type := { Ty : Type }. +Instance: some_type := { Ty := nat }. +Arguments Ty : clear implicits. +Goal forall (H : forall t : some_type, @Ty t -> False) (H' : False -> 1 = 2), 1 = 2. +Proof. +intros H H'. +specialize (H' (@H _ O)). (* was failing *) diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index fba05cd90..4b41a509e 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -72,3 +72,11 @@ intros. specialize (H 1) as ->. reflexivity. Qed. + +(* A test from corn *) + +Goal (forall x y, x=0 -> y=0 -> True) -> True. +intros. +specialize (fun z => H 0 z eq_refl). +exact (H 0 eq_refl). +Qed. |