aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Collapse)Author
2014-02-02Fixing backtrace reporting.Pierre-Marie Pédrot
2014-01-31Typos in comment.Arnaud Spiwack
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2014-01-10Useless Array.of_listPierre-Marie Pédrot
2014-01-10Exporting the full pretyper options in Goal.constr_of_raw.Pierre-Marie Pédrot
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-06Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, ↵Arnaud Spiwack
without" This reverts commit bfe1141026da70d8f59cf47b5fe61ffc20a29f3c. Conflicts: proofs/proofview_monad.ml This is potentially a temporary commit until a final decision is taken on hand-written versus extracted ocaml for the tactic monad. The hand-written implementation has a bug where the + tactical would not behave properly (I tried to find why, but couldn't: the hand-written implementation looks fine, but it isn't. Beats me). There is a conflict with Pierre-Marie's commit 4832692: Fixing backtrace registering of various tactic-related try-with blocks.
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
Proof using can be followed by: - All : all variables - Type : all variables occurring in the type - expr: - (a b .. c) : set - expr + expr : set union - expr - expr : set difference - -expr : set complement (All - expr) Exceptions: - a singleton set can be written without parentheses. This also allows the implementation of named sets sharing the same name space of section hyps ans write - bla - x : where bla is defined as (a b .. x y) elsewhere. - if expr is just a set, then parentheses can be omitted This module also implements some AI to tell the user how he could decorate "Proof" with a "using BLA" clause. Finally, one can Set Default Proof Using "str" to any string that is used whenever the "using ..." part is missing. The coding of this sucks a little since it is the parser that applies the default.
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
To make this possible the state id has to reach the kernel. Hence definition_entry has an extra field, and many files had to be fixed.
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
Actually, this was wrong, as evars should not appear until interpretation. Evarmaps were only passed around uselessly, and often fed with dummy or irrelevant values.
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-04Fix Admitted.Arnaud Spiwack
Commit "The commands that initiate proofs…" was a bit hasty in its treatment of Admitted (in an attempt of making things simple, I actually required the proof to be completed for Admitted to go through…).
2013-12-04Proof_global: fix start_proof comment after the preceding commits.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
This commit removes the hook.
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command. In this commit, we remove the compute_guard parameter.
2013-12-04The commands that initiate proofs are now in charge of what happens when ↵Arnaud Spiwack
proofs end. The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it. In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands. In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
2013-11-30Fixing ltac constr variable handling in refine.Pierre-Marie Pédrot
2013-11-29Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notHugo Herbelin
supporting metas/evars). Fix of #3169 is by calling pretyping retyper rather than the non evar-aware kernel type-checker (since argument of vm_compute is supposed to be already typable). Support of metas/evars in vm is still to be done...
2013-11-12Useless computation in Goal handle augmentation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17083 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17082 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-09Partial applications in Goal.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17074 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-07Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutppedrot
going through a Coq extraction phase. We use second order quantification through OCaml records, which allows for a very precise use of low-level application. This results in quite a remarkable speedup but there is still room for improvement. This code was written by translating straightforwardly the Coq generated code in a human-readable dialect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17068 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-06Less partial applications in Vars, as well as better memory allocation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-05Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same timeppedrot
the argument list is consumed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17062 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was ↵aspiwack
solved. This made "autorewrite using tac" fail. Spotted in CoLoR and Demos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Fix the tactical ; [ … ] : the "incorrect number of goal" error was not ↵aspiwack
caught by ltac tacticals. The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad). Spotted in ProjectiveGeometry and Goedel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17057 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-04Allowing proofs starting with a non-empty evarmap.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A try/with was catching every exception.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17034 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Update comments.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Doc: solve the bad interaction between Declare Implicit Tactic and refine.aspiwack
An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17032 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Fix destruct: nf_evar prior to tactic interpretation.aspiwack
Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Add primitives in Goal.V82 to access the goal in nf_evar'd form.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17025 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactic give_up.aspiwack
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A tactic shelve_unifiable.aspiwack
Puts on the shelf every goals under focus on which other goals under focus depend. Useful when we want to solve these goals by unification (as in a first order proof search procedure, for instance). Also meant to be able to recover approximately the semantics of the old refine with the new implementation (use refine t; shelve_unifiable). TODO: bug dans l'example de shelve_unifiable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ↵aspiwack
at the wrong time. The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t)) had the correct semantics! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17014 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a shelve tactic.aspiwack
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02bootstrap/Monad.v: implements the writer monad in continuation passing style.aspiwack
Benefits: fewer pair constructed/destructed especially in split. Potential costs: plus and zero now have closures with 11 arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17012 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02bootstrap/Monad.v: implements the environment monad in continuation passing ↵aspiwack
style. Benefits: the underlying monads are not referenced in the "current" primitive. Potential costs: some extracted functions now have 9 arguments, Ocaml may not be good at handling these. The split primitive, which is called often, now builds one extra closure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17011 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds an experimental exactly_once tactical.aspiwack
exactly_once t, will have a success if t has exactly once success. There are a few caveats: - The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics) - The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17009 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Normalise goals with respect to evars in the new tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17008 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Made Proofview.Goal.hyps a named_context.aspiwack
There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A dedicated view type for Proofview_gen.split.aspiwack
It doesn't seem to affect performances. But the generated code is slightly cleaner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17005 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a tactical once.aspiwack
[once t] does just as [t] but has exactly one success it [t] has at least one success. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17004 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
As a result the use of the glist-style interface for manipulating goals has almost been removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02More Proofview.Goal.enter.aspiwack
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad. This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics. This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02A better version of Goal.advance.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16999 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 14:24:55 +0000