diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-12 11:53:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-30 14:40:45 +0200 |
| commit | be73d7eccd3e3165ce719b36910920e05cf416bc (patch) | |
| tree | e4080480250a13e90fa326b92697ff524f6a35ca /plugins/ltac/tacsubst.ml | |
| parent | 9a63fdf0cad004d21ff9e937b08e7758e304bcd3 (diff) | |
Adding "epose", "eset", "eremember" which allow to set terms with
evars.
This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.
Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
Diffstat (limited to 'plugins/ltac/tacsubst.ml')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 1ae792971..f5e6f05ce 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -151,8 +151,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacLetTac (id,c,clp,b,eqpat) -> - TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) + | TacLetTac (ev,id,c,clp,b,eqpat) -> + TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat) (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> |