aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing inclusion of user contrib directory in the loadpath.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-03-31
* A more reasonable implementation of Loadpath.Gravatar Pierre-Marie Pédrot2015-03-31
* Declarative mode: fix proof modes.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: fix vernac classification.Gravatar Arnaud Spiwack2015-03-31
* Declarative mode: plug the specialised printers back.Gravatar Arnaud Spiwack2015-03-31
* Better formatting of messages in proofs.Gravatar Arnaud Spiwack2015-03-31
* Generalisation of the "end command" argument of the goal printer.Gravatar Arnaud Spiwack2015-03-31
* Fix various typos in documentationGravatar Matěj Grabovský2015-03-31
* Do not escape "'" when outputting to html, especially not using "´".Gravatar Guillaume Melquiond2015-03-31
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
* camlp4: grep away warnings in output/* testsGravatar Enrico Tassi2015-03-30
* coq_makefile: fix compilation with camlp4Gravatar Enrico Tassi2015-03-30
* fix code and bound for SWITCH instruction.Gravatar Benjamin Gregoire2015-03-30
* Ensuring more invariants in Constr_matching.Gravatar Pierre-Marie Pédrot2015-03-29
* Adding test for bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Fixing bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* Normalize scope names before storing them in vo files. (Fix for bug #4162)Gravatar Guillaume Melquiond2015-03-27
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* STM: refine the notion of "simply a tactic"Gravatar Enrico Tassi2015-03-27
* Properly handle extra "clean" targets with coq_makefile.Gravatar Guillaume Melquiond2015-03-27
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* allows the vm to deal with inductive type with 8388607 constant constructors ...Gravatar Benjamin Gregoire2015-03-26
* fix compilationGravatar Benjamin Gregoire2015-03-26
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* add coqdep in distributed_exec, else make does not work.Gravatar Benjamin Gregoire2015-03-26
* STM: change how proof mode switching commands are handled (decl_mode)Gravatar Enrico Tassi2015-03-26
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* More clever representation of substituted Cemitcode.Gravatar Pierre-Marie Pédrot2015-03-25
* Summary: fix code to detect functional values in summaryGravatar Enrico Tassi2015-03-25
* STM: avoid processing asynchronously empty proofs (Close: #4134)Gravatar Enrico Tassi2015-03-25
* Exporting memory representation of STM tasks for votour.Gravatar Pierre-Marie Pédrot2015-03-25
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Another example about the consequence of a wrong computation of theGravatar Hugo Herbelin2015-03-25
* Use kernel names instead of user names when looking for coercions. (Fix for b...Gravatar Guillaume Melquiond2015-03-25
* coqc: fix --helpGravatar Enrico Tassi2015-03-25
* Correcting a bug introduced by universes polymorphismGravatar jforest2015-03-25
* correcting a bug with aliased when using Functional SchemeGravatar forest2015-03-25
* Updating test-suite (see previous commit).Gravatar Hugo Herbelin2015-03-24
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
* Functorized interface over object representation in votour.Gravatar Pierre-Marie Pédrot2015-03-24
* Fixing representation of dynamics in votour (again).Gravatar Pierre-Marie Pédrot2015-03-24
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 05:05:58 +0000