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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 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) |