diff options
| author | Emilio Jesus Gallego Arias | 2019-02-13 05:37:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | c0cff3a7ebb79d1142090108c56e9aa64c3b481d (patch) | |
| tree | b316f32c8c5d879324031dd17ca317cb29ce4b1f /proofs | |
| parent | 178672504f1c92b162c2575b14034cc7b698b6a4 (diff) | |
[geninterp] Track polymorphic status in tactic interpretation.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0f97a942ed..1a34105ab6 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -55,6 +55,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.fail_evar = false; Pretyping.expand_evars = true; Pretyping.program_mode = false; + Pretyping.polymorphic = false; } in try Pretyping.understand_ltac flags env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 0fefb215e2..86d3d9601e 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -85,7 +85,7 @@ let with_current_proof f (ps, psl) = | None -> Proofview.tclUNIT () | Some tac -> let open Geninterp in - let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in + let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in let tac = Geninterp.interp tag ist tac in Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) |