diff options
| author | Pierre-Marie Pédrot | 2016-04-25 10:55:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 12:18:26 +0200 |
| commit | a7917a32b24b652d2978a7aea171aa01da37eece (patch) | |
| tree | 562151497aed2a7ae06e58ee4f25032f46afc335 /pretyping | |
| parent | 27d4a57975ab5919d81f9951b430a35d1067e846 (diff) | |
Merging the ML tactic notation and plain Tactic Notation mechanisms.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8baa668c7b..5e6a3eac73 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1126,7 +1126,7 @@ let type_uconstr ?(flags = constr_flags) ltac_constrs = closure.typed; ltac_uconstrs = closure.untyped; ltac_idents = closure.idents; - ltac_genargs = ist.Geninterp.lfun; + ltac_genargs = Id.Map.empty; } in let sigma = Sigma.to_evar_map sigma in let (sigma, c) = understand_ltac flags env sigma vars expected_type term in |