diff options
author | 2016-04-12 22:25:26 +0200 | |
---|---|---|
committer | 2016-04-27 21:55:45 +0200 | |
commit | bde36d4b00185065628324d8ca71994f84eae244 (patch) | |
tree | c4d7bba0352ee72fa31712e02882c7066a6e1ba1 /ltac/tacsubst.ml | |
parent | c4d1e3113f77af2e5474fe5676c272050dd445e5 (diff) |
In the short term, stronger invariant on the syntax of TacAssert, what
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
Diffstat (limited to 'ltac/tacsubst.ml')
-rw-r--r-- | ltac/tacsubst.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 438219f5a..22660aa83 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -151,7 +151,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | 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 (subst_tactic subst) otac,na,subst_glob_constr subst c) + TacAssert (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) | TacLetTac (id,c,clp,b,eqpat) -> |