diff options
| author | Hugo Herbelin | 2015-11-07 22:21:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-07 22:26:03 +0100 |
| commit | 479d4cd6e9934a47debf6201fccf7ebb1aea1b09 (patch) | |
| tree | a2bc3eb59a3ff6c409a488344432f30c6b2ab772 | |
| 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.
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index a38a36bdcc..e80f5a64c7 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -532,7 +532,7 @@ let prim_refiner r sigma goal = push_named_context_val (id,None,t) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in + let oterm = Term.mkNamedLetIn id ev1 t ev2 in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5f7fcce572..936c5988f6 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.") |