diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 13 | ||||
| -rw-r--r-- | proofs/refine.mli | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 |
4 files changed, 9 insertions, 10 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c36b0fa337..b022f4596d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -19,7 +19,7 @@ open Reduction open Clenv (* This function put casts around metavariables whose type could not be - * infered by the refiner, that is head of applications, predicates and + * inferred by the refiner, that is head of applications, predicates and * subject of Cases. * Does check that the casted type is closed. Anyway, the refiner would * fail in this case... *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 52e15f466f..7333114eae 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -142,12 +142,11 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in - let ce = - if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce - else { ce with - const_entry_body = Future.chain ce.const_entry_body - (fun (pt, _) -> pt, ()) } in - let (cb, ctx), () = Future.force ce.const_entry_body in + let body = Future.force ce.const_entry_body in + let (cb, ctx) = + if side_eff then Safe_typing.inline_private_constants env body + else fst body + in let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs @@ -197,5 +196,5 @@ let refine_by_tactic ~name ~poly env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) - let ans = Safe_typing.inline_private_constants_in_constr env ans neff in + let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in ans, sigma diff --git a/proofs/refine.mli b/proofs/refine.mli index 55dafe521f..b8948a92f3 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -9,7 +9,7 @@ (************************************************************************) (** The primitive refine tactic used to fill the holes in partial proofs. This - is the recommanded way to write tactics when the proof term is easy to + is the recommended way to write tactics when the proof term is easy to write down. Note that this is not the user-level refine tactic defined in Ltac which is actually based on the one below. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bce227dabb..799f4a380b 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -289,7 +289,7 @@ let tclIFTHENTRYELSEMUST tac1 tac2 gl = (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first thats solves the current goal *) +(* Try the first that solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) |