diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-07 22:21:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-07 22:26:03 +0100 |
| commit | 479d4cd6e9934a47debf6201fccf7ebb1aea1b09 (patch) | |
| tree | a2bc3eb59a3ff6c409a488344432f30c6b2ab772 /tactics | |
| parent | c23f0cab6ee1e9c9b63347cd2624b64591871cb1 (diff) | |
Implementing assert and cut with LetIn rather than using a beta-redex.
Hopefully, it will provide with nicer proof terms, in combination with
the commit printing the type of LetIn when the defined term is a proof.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5f7fcce57..936c5988f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1062,8 +1062,8 @@ let cut c = Proofview.Refine.refine ~unsafe:true { run = begin fun h -> let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in let Sigma (x, h, q) = Evarutil.new_evar env h c in - let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in - Sigma (mkApp (f, [|x|]), h, p +> q) + let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in + Sigma (f, h, p +> q) end } else Tacticals.New.tclZEROMSG (str "Not a proposition or a type.") |