aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-07-12 11:40:52 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-30 14:40:45 +0200
commit9a63fdf0cad004d21ff9e937b08e7758e304bcd3 (patch)
treeaa0c3c17642a1a86f4170af1423f2da5ea67c45e /plugins
parentfd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff)
Adding "eassert", "eenough", "epose proof", which allow to state
a goal with unresolved evars.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/g_tactic.ml427
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml4
-rw-r--r--plugins/ltac/tacinterp.ml18
-rw-r--r--plugins/ltac/tacsubst.ml4
6 files changed, 39 insertions, 24 deletions
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1404b1c1f..c6a3beb89 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -552,24 +552,39 @@ GEXTEND Gram
(* Alternative syntax for "pose proof c as id" *)
| IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
c = lconstr; ")" ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+ | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+ c = lconstr; ")" ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "assert c as id by tac" *)
| IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+ | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ c = lconstr; ")"; tac=by_tactic ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
(* Alternative syntax for "enough c as id by tac" *)
| IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
c = lconstr; ")"; tac=by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+ | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+ c = lconstr; ")"; tac=by_tactic ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
| IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
+ | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c))
| IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c))
+ | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c))
| IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c))
+ | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
+ TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
| IDENT "generalize"; c = constr ->
TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2b..22ecf61aa 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -768,15 +768,15 @@ type 'a extra_genarg_printer =
primitive "cofix" ++ spc () ++ pr_id id ++ spc()
++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
)
- | TacAssert (b,Some tac,ipat,c) ->
+ | TacAssert (ev,b,Some tac,ipat,c) ->
hov 1 (
- primitive (if b then "assert" else "enough") ++
+ primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
)
- | TacAssert (_,None,ipat,c) ->
+ | TacAssert (ev,_,None,ipat,c) ->
hov 1 (
- primitive "pose proof"
+ primitive (if ev then "epose proof" else "pose proof")
++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
)
| TacGeneralize l ->
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index bf760e7bb..11e7278d9 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -141,7 +141,7 @@ type 'a gen_atomic_tactic_expr =
| TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
| TacMutualCofix of Id.t * (Id.t * 'trm) list
| TacAssert of
- bool * 'tacexpr option option *
+ evars_flag * bool * 'tacexpr option option *
'dtrm intro_pattern_expr located option * 'trm
| TacGeneralize of ('trm with_occurrences * Name.t) list
| TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e431a13bc..734ce46e4 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -489,8 +489,8 @@ let rec intern_atomic lf ist x =
| TacMutualCofix (id,l) ->
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
TacMutualCofix (intern_ident lf ist id, List.map f l)
- | TacAssert (b,otac,ipat,c) ->
- TacAssert (b,Option.map (Option.map (intern_pure_tactic ist)) otac,
+ | TacAssert (ev,b,otac,ipat,c) ->
+ TacAssert (ev,b,Option.map (Option.map (intern_pure_tactic ist)) otac,
Option.map (intern_intro_pattern lf ist) ipat,
intern_constr_gen false (not (Option.is_empty otac)) ist c)
| TacGeneralize cl ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d1..d4ed77015 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -672,10 +672,7 @@ let pure_open_constr_flags = {
expand_evars = false }
(* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
- let flags =
- if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
- else open_constr_use_classes_flags () in
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
interp_gen expected_type ist false flags env sigma c
let interp_pure_open_constr ist =
@@ -1727,18 +1724,21 @@ and interp_atomic ist tac : unit Proofview.tactic =
Sigma.Unsafe.of_pair (tac, sigma)
end }
end
- | TacAssert (b,t,ipat,c) ->
+ | TacAssert (ev,b,t,ipat,c) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
- let (sigma,c) =
- (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
+ let (sigma,c) =
+ let expected_type =
+ if Option.is_empty t then WithoutTypeConstraint else IsType in
+ let flags = open_constr_use_classes_flags () in
+ interp_open_constr ~expected_type ~flags ist env sigma c
in
let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
let tac = Option.map (Option.map (interp_tactic ist)) t in
- Tacticals.New.tclWITHHOLES false
+ Tacticals.New.tclWITHHOLES ev
(name_atomic ~env
- (TacAssert(b,Option.map (Option.map ignore) t,ipat,c))
+ (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c))
(Tactics.forward b tac ipat' c)) sigma
end }
| TacGeneralize cl ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4390ff08b..1ae792971 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
| TacMutualCofix (id,l) ->
TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
- | TacAssert (b,otac,na,c) ->
- TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na,
+ | TacAssert (ev,b,otac,na,c) ->
+ TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na,
subst_glob_constr subst c)
| TacGeneralize cl ->
TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)