diff options
| author | Pierre-Marie Pédrot | 2015-12-17 19:24:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-21 19:36:38 +0100 |
| commit | b2beb9087628de23679a831e6273b91816f1ed27 (patch) | |
| tree | 40784a3be039885aef29c3c23fda2a0189fe2ac1 /grammar | |
| parent | fcf425a4714f0c888b3d670a9a37fe52a6e49bc5 (diff) | |
Using dynamic values in tactic evaluation.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a49291d947..fff7068571 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -194,7 +194,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it (Genarg.in_gen $make_globwit loc globtyp$ x) in - (sigma , out_gen $make_topwit loc globtyp$ a_interp)>> + (sigma , Tacinterp.Value.cast $make_topwit loc globtyp$ a_interp)>> end | Some f -> <:expr< $lid:f$>> in let subst = match h with diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index df2209606d..01828267bf 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -53,7 +53,7 @@ let rec make_let raw e = function let e = make_let raw e l in let v = if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in + else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l @@ -73,7 +73,7 @@ let check_unicity s l = let make_clause (pt,_,e) = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let false e pt) let make_fun_clauses loc s l = |