diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-11 14:47:52 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-18 20:22:40 +0200 |
| commit | 4a76d2034983462175219426ec47c45a3c60d4fe (patch) | |
| tree | aaf466532522a6a169bf8c405912aed0281912a2 /plugins/decl_mode | |
| parent | 7cfb1c359faf13cd55bd92cba21fb00ca8d2d0d2 (diff) | |
Constraining refine to monotonic functions.
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index d8c5b8a95..1741df533 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -29,6 +29,7 @@ open Termops open Namegen open Goptions open Misctypes +open Sigma.Notations (* Strictness option *) @@ -1305,7 +1306,11 @@ let understand_my_constr env sigma c concl = Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) let my_refine c gls = - let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + let oc = { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + Sigma.Unsafe.of_pair (c, sigma) + end } in Proofview.V82.of_tactic (Tactics.New.refine oc) gls (* end focus/claim *) |