aboutsummaryrefslogtreecommitdiff
path: root/plugins/subtac
AgeCommit message (Collapse)Author
2012-04-12remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15129 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
Migrate the backtracking code from ide_slave.ml into a new backtrack.ml. In particular the history stack of commands that used to be there is now non-coqide-specific. ** Adapted commands ** - "Show Script": a basic functional version is restored (and the printing of scripts at Qed in coqtop). No indentation, one Coq command per line, based on the vernac_expr asts recorded in the history stack, printed via Ppvernac. - "Back n" : now mimics the backtrack of coqide: it goes n steps back (both commands and proofs), and maybe more if needed to avoid re-entering a proof (it outputs a warning in this case). - "BackTo n" : still try to go back to state n, but it also handles the proof state, and it may end on some state n' <= n if needed to avoid re-entering a proof. Ideally, it could someday be used by ProofGeneral instead of the complex Backtrack command. ** Compatible commands ** - "Backtrack" is left intact from compatibility with current ProofGeneral. We simply re-synchronize the command history stack after each Backtrack. - "Undo" is kept as a standard command, not a backtracking one, a bit like "Focus". Same for "Restart" and "Abort". All of these are now accepted in coqide (Undo simply triggers a warning). - Undocumented command "Undo To n" (counting from start of proof instead of from end) also keep its semantics, it is simply made compatible with the new stack mechanism. ** New restrictions ** We now forbid backtracking commands (Reset* / Back*) inside files when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail. Too much work dealing with these situation that nobody uses. ** Internal details ** Internally, the command stack differs a bit from what was in Ide_slave earlier (which was inspired by lisp code in ProofGeneral). We now tag commands that are unreachable by a backtrack, due to some proof being finished, aborted, restarted, or partly Undo'ed. This induce a bit of bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code is straightforward: we simply search backward the first reachable state starting from the desired place. We don't depend anymore on the proof names (apart in the last proof block), It's more robust this way (think of re-entering a M.foo from an outside proof foo). Many internal clarifications in Lib, Vernac, etc. For instance "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls (Lib.label_before_name "foo"), and performs a BackTo to the corresponding label. Concerning Coqide, we directly suppress the regular printing of goals via a flag in Vernacentries. This avoid relying on a classification of commands in Ide_slave as earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Fix merge.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15039 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution ↵msozeau
of evars. Used when interpreting a constr in Ltac: resolution is now launched if the constr is casted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Final part of moving Program code inside the main code. Adapted ↵msozeau
add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to ↵msozeau
toplevel/ The code is not called yet from there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Second step of integration of Program:msozeau
- Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-14Remove support for "abstract typing constraints" that requires unicity of ↵msozeau
solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-02Noise for nothingpboutill
Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-20Correct application of head reduction.msozeau
Fix a regression in subtac_pretyping, avoiding application of bidirectional application checking in case the return type is a subset (bad interaction with typeclass overloading). Should be done only on constructor applications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14985 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-15Avoid retrying uncessarily to prove independent remaining obligations in ↵msozeau
Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14982 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-15Avoid unnecessary normalizations w.r.t. evars in Program.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14981 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-14- Fix dependency computation in eterm to not consider filtered variables.msozeau
- Fix handling of evar map in Program coercion code that could forget some new declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14978 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Fix camlp4 compilationpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14951 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fix for Program Instance not separately checking the resolution of evars of ↵msozeau
the type (mandatory) and the fields (optional) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14940 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Another quick hack that works this time, to handle printing of locality in ↵ppedrot
Program subtac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14939 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20Reverted previous commit, which broke library compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-20This is a quick hack to permit the parsing of the locality flag in the ↵ppedrot
Program subtactic. Ideally, locality flags should be handled in a nicer way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14924 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-17Fixed the pretty-printing of the Program plugin.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-12Proof using ...gareuselesinge
New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14749 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options ↵ppedrot
are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14571 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
function but also restricting it to closed matching and consequently renaming it to subst_closed_term_occ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14498 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23Fix commit 14489: missing Coq. in dirpathletouzey
Kudos to Tom Prince for noticing this... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14491 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-23Program: add some check_required_library (fix #2592) + some dead code removalletouzey
If these additional checks take too much time, maybe using true laziness instead of (fun () -> ...) could help. Btw, some other init_constant in Program would deserve preliminary check_required_library... I've also removed some unused delayed constr, at least one of them being erroneous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14489 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-29Subtac_cases: replaced some generic = on constr by destructorspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14363 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Fix compilation errormsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14252 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-30Keep obligation source information in Programmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14251 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
particular, new printer for evar_map which displays undefined evars + defined evars that were instantiated by these undefined evars and recursively, up to some arbitrary level n chosen to be in practice n=2 (thanks to Arnaud). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14231 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-17Fix bug 2269, program typechecker not used in Instance conclusionsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14212 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
plugins so that errors are indeed processed. Not sure this is the best way to do it. Maybe funind should use with_heavy_rollback for delimitating its use of vernac commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14181 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fix bug #2399 in Program: used to build an ill-formed term due to a de ↵msozeau
Bruijn bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14168 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-07Fix bug #2415: warn when closing modules or sections and some obligations ↵msozeau
are unresolved git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14165 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-13A new mechanism to handle errors.aspiwack
Instead of the monolitic Cerrors, I introduce a lightweight Errors module whose error message can be expanded by module introducing exceptions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719. Conflicts: kernel/term_typing.ml test-suite/success/polymorphism.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13Add [Polymorphic] flag for defsmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
when a "match" is kernel-ill-typed (probably rarely visible from end user anyway but useful for debugging) + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-07Extraction: unfolds the let-in created by Program when handling "match"letouzey
This leads to code closer to the original input of the user, and moreover some more dummy __ may be removed this way. To avoid unfolding by mistake user's variables, we change the name of these generated let-in into "program_branch_NN" instead of "branch_NN" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13964 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
in preparation for adding forward reasoning to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:09:26 +0000