aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Fixing an interpretation bug with tactics in notations. For some obscureGravatar Pierre-Marie Pédrot2014-01-19
| | | | | | reason, Ltac interpretation does not allow tactics of the following shape : let x := bla in TacGeneric tac. Hence we force genargs to be tactics and build the resulting hole tactic from scratch.
* Fixing checker compilation, which was broken by the following commit:Gravatar Pierre-Marie Pédrot2014-01-19
| | | | 05d5f8b9065b0f5e0349cf3d39dd62ab99f30369
* Relaxing the sort elimination check to allow for let-bindings in arities.Gravatar Maxime Dénès2014-01-18
| | | | | | | I restored this in the kernel, and added it to the checker. There is one last source of non-uniformity, which is the Sort case in the checker (was not present in the kernel). I don't know what this case covers, so it should be reviewed.
* Makefiles use $(foo), not $foo, for variablesGravatar Jason Gross2014-01-18
| | | | | | Also, we need :=, so that it's evaluated immediately, rather than becoming a self-recursive variable. This fixes the "Undefined variable 'C'" error that make keeps spewing.
* Fixup make clean and .merlinGravatar Pierre Boutillier2014-01-18
|
* Follow-up of bugfix for #3204: local definitions were not handled properly.Gravatar Pierre-Marie Pédrot2014-01-17
|
* Fixing bug #1758: Print Hint output can be misleading if variable shadows ↵Gravatar Pierre-Marie Pédrot2014-01-17
| | | | hypothesis.
* Update .mailmap with recent contributors.Gravatar Arnaud Spiwack2014-01-17
| | | | | I should have updated everyone who committed since the migration to git (giving me a canonical email). I've search git shortlog -s to ensure the best I could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed.
* Fixing bugs #1039: Hypotheses don't respect Barendregt conventionGravatar Pierre-Marie Pédrot2014-01-16
| | | | | | and #3204: Failure of hygiene condition. It was sufficient to tweak a flag in the constr externalization...
* Implementing transitive reduction in the dependency graph printingGravatar Pierre-Marie Pédrot2014-01-16
| | | | mechanism of coqdep.
* Christmas is over...Gravatar Maxime Dénès2014-01-15
|
* Test case containing a proof of false due to a DeBruijn off-by-one error in theGravatar Maxime Dénès2014-01-15
| | | | code checking allowed sorts for elimination.
* -schedule-vi-checking generates better scriptGravatar Enrico Tassi2014-01-14
|
* STM: fix -async-proofs lazyGravatar Enrico Tassi2014-01-14
|
* Removing unused tactics in rewrite.Gravatar Pierre-Marie Pédrot2014-01-14
|
* Make Require verboseGravatar Pierre Boutillier2014-01-13
|
* rename Paral-ITP demo fileGravatar Enrico Tassi2014-01-13
|
* Paral-ITP demo: better commentsGravatar Enrico Tassi2014-01-13
|
* STM: fix very simple demoGravatar Enrico Tassi2014-01-13
|
* Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Gravatar Pierre Boutillier2014-01-13
| | | | The exact filename has to be written. This is coherent with the RefMan.
* Fixing typo in reference manual from previous commitGravatar Hugo Herbelin2014-01-13
|
* Documenting old but useful command "Print Tables".Gravatar Hugo Herbelin2014-01-13
| | | | | Made a synonymous of it ("Print Options"). Also reorganized a bit the section about flags and options in reference manual.
* 'Pretty' printer for wf_pathsGravatar Pierre2014-01-11
|
* Fixing bug #3144.Gravatar Pierre-Marie Pédrot2014-01-10
|
* Useless Array.of_listGravatar Pierre-Marie Pédrot2014-01-10
|
* Omega: avoiding distinct proof-terms on repeated identical runsGravatar Pierre Letouzey2014-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Omega now reuse the same inner variable names (Zvar0, Zvar1, ...) at each run. This way, the obtained proof-terms on two identical omega runs should be the same. This wasn't always the case earlier: - the two proofs were almost always convertible, but with distinct variable names. - in very rare situations, the two proofs could even be non-convertible. Indeed, the omega engine use hash-tables which may be sensible to the names in the (in)equality system and hence lead to different solutions. Example of this behavior (with ocaml 4, whose default hash function is different from ocaml 3.12, leading to a different behavior here !) : -------------------------------------------------------------------- Require Import Omega. Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined. Check (eq_refl : test1 = test2). (* OK *) Check (eq_refl : test1 = test3). (* OK *) Check (eq_refl : test1 = test4). (* KO, test4 is different !! *) -------------------------------------------------------------------- The old behavior could be restored with "Unset Stable Omega". Thanks to Frédéric Loulergue for spotting this sensibility to the underlying ocaml versions...
* Exporting the full pretyper options in Goal.constr_of_raw.Gravatar Pierre-Marie Pédrot2014-01-10
|
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10
|
* Goodbye typerex, Hello merlinGravatar Pierre2014-01-09
|
* md5 for MacOSGravatar Pierre2014-01-09
| | | | md5sum check remains not portable.
* Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evdGravatar Pierre Letouzey2014-01-08
|
* typosGravatar Enrico Tassi2014-01-07
|
* STM: additional fix for STM + vm_computeGravatar Enrico Tassi2014-01-07
| | | | | | | Thanks again Maximes. This time the C value was stored in the env_(named|rel)_val of the environment
* Adding a -dumpgraph option to Coqdep that output the graph dependency of theGravatar Pierre-Marie Pédrot2014-01-06
| | | | | | considered files. Original patch by Guillaume Allais.
* CoqIDE: do not unfocus if not needed on errors (closes: 3197)Gravatar Enrico Tassi2014-01-06
|
* fix simple test for paral-itpGravatar Enrico Tassi2014-01-06
|
* fix typoGravatar Enrico Tassi2014-01-06
|
* STM: handle side effects of workers correctlyGravatar Enrico Tassi2014-01-06
|
* STM: fix worker crash when doing vm_computeGravatar Enrico Tassi2014-01-06
| | | | | | | | | | Kudos to Maximes for finding the culprit in no time! Values of type 'Pre_env.key' store in the OCaml state the 'address' of an already evaluated constant in the VM's C state. Such values are not sent to work processes. The worker is going to re-evaluate the constant, but just once, since the cache is cleared only when the env is marshalled (via ephemerons).
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
|
* Add a test suite file for Ltac's "+" tactical.Gravatar Arnaud Spiwack2014-01-06
|
* Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, ↵Gravatar Arnaud Spiwack2014-01-06
| | | | | | | | | | | | | 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.
* refman: fist stab at Asynchronous ProofsGravatar Enrico Tassi2014-01-05
|
* STM: modules do not prevent proofs from being ASyncGravatar Enrico Tassi2014-01-05
|
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* Fix coqc -time (Closes: 3201)Gravatar Enrico Tassi2014-01-05
|
* nanoPG: compete rewriting with more Emacs/PG like featuresGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not possible to add shortcuts with arbitrary modifiers and to save into a state some data, like the line offset for C-n and the killed text for C-k and C-y. If you see that your favorite Emacs/PG shortcut is missing, please tell me! Currently supported shortcuts: C-_ Undo C-g Esc C-s Search C-e Move to end of line M-e Move to end of sentence M-a Move to beginning of sentence C-n Move to next line C-p Move to previous line C-f Forward char C-b Backward char M-f Forward word M-b Backward word C-k Kill untill the end of line M-d Kill next word M-k Kill until sentence end M-DELBACK Kill word before cursor C-d Delete next character C-y Yank killed text back C-c C-RET Go to C-c C-n Advance 1 sentence C-c C-u Retract 1 sentence C-c C-b Advance C-c C-r Restart C-c C-c Stop C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-b About C-c C-a C-a Search About C-c C-a C-o Search Pattern C-c C-a C-l Locate C-c C-a C-RET match template C-x C-s Save C-x C-c Quit C-x C-f Open
* Disable GlobRef feedback (CoqIDE does nothing with them)Gravatar Enrico Tassi2014-01-05
| | | | | | The original idea was to send not the kernel name, but the file/line to that CoqIDE could make the text an hyperlink to the file, exactly as coqdoc generated HTML.
* Environ: export API to transitively close a set of section variablesGravatar Enrico Tassi2014-01-05
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 06:23:55 +0000