aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\
| * Moving back Ltac profiling to the Ltac folder.Gravatar Pierre-Marie Pédrot2016-06-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \
| * | Tentatively fixing misguiding error message with "binder" type inGravatar Hugo Herbelin2016-06-13
| * | Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
| * | Fixing bug in printing CannotSolveConstraint (collision of context names).Gravatar Hugo Herbelin2016-06-12
* | | Search interface revisions.Gravatar Pierre-Marie Pédrot2016-06-07
|\ \ \
| * | | Removing the convenience functions from the Search API.Gravatar Pierre-Marie Pédrot2016-06-07
| | * | Fixing problems introduced in 8.5 with Ltac trace report. E.g.Gravatar Hugo Herbelin2016-06-06
| | | * -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
| | | * LtacProf for Coq trunkGravatar Jason Gross2016-06-05
| |_|/ |/| |
* | | coqtop: Add ltac/ to search path.Gravatar Matthieu Sozeau2016-06-02
| | * Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | | Put the "exact_constr" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\ \ \ | | |/ | |/|
| * | Fix bug #3887: Better error message for "More than one program with unsolved ...Gravatar Pierre-Marie Pédrot2016-05-09
| * | Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
| * | Call hooks when terminating a definition proof (bug #4663).Gravatar Guillaume Melquiond2016-05-03
| * | Properly handle notations containing spaces (bug #4538).Gravatar Guillaume Melquiond2016-05-02
* | | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* | | Revert "Protect the beautifier from change in the lexer state (typically by"Gravatar Hugo Herbelin2016-04-27
* | | Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-04-27
* | | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
| | * avoid communicating to the serarch interface using raw strings.Gravatar Gregory Malecha2016-04-24
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Building lazily a few debugging messages involving expressions of commandsGravatar Hugo Herbelin2016-04-17
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
|\|
| * Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
* | Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkGravatar Matej Kosik2016-04-04
|\ \
* \ \ Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...Gravatar Matej Kosik2016-04-04
|\ \ \
| | * | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
| |/| | |/| | |
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\ \ \ \ | | |_|/ | |/| |
* | | | Was too restrictive in syntactic definitions, not imagining that theyGravatar Hugo Herbelin2016-03-28
| * | | Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* | | | Moving Tactic_debug to Hightactic.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-20
|\| | |
* | | | Moving Tacintern to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving the tactic related code from Metasyntax to a new file.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | | | Moving Tacinterp to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20