aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-25 16:06:47 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-25 16:06:47 +0200
commit4ad6dbef69f9fd4cb1b55efc252d67325068e6b1 (patch)
tree0c2c1f2310cf5751a2f97f29a0bfd5a8295d1da2
parent48d56f49b1db47f393ef3e0f31d1b22adf497afa (diff)
parent5c5f7c8d6a6ed8cbb99b12dde09fdbcc30ca8ab9 (diff)
Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings
-rw-r--r--CHANGES4
-rw-r--r--dev/doc/changes.txt6
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli5
-rw-r--r--plugins/ltac/tacinterp.ml18
-rw-r--r--tactics/tactics.ml3
-rw-r--r--test-suite/bugs/closed/5153.v8
-rw-r--r--test-suite/success/specialize.v8
8 files changed, 46 insertions, 8 deletions
diff --git a/CHANGES b/CHANGES
index 0b55183f3..30bea7a7b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.