aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* sed s'/_one_var/_on/g'Gravatar Jason Gross2014-08-26
* Generalize EqdepFactsGravatar Jason Gross2014-08-26
* Do not pass "-batch" or "-load-vernac-source" to slaves, avoiding errors inGravatar Matthieu Sozeau2014-08-26
* Make evarconv and unification able to handle eta for records in presenceGravatar Matthieu Sozeau2014-08-26
* Fix compilation error due to commented code in previous commit by Hugo.Gravatar Matthieu Sozeau2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fix computation of dangling constraints at the end of a proof (bug #3531).Gravatar Matthieu Sozeau2014-08-25
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* Add an is_cofix tacticGravatar Jason Gross2014-08-25
* Prerequisite to fix stm test-suite when not in -localGravatar Pierre Boutillier2014-08-25
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Clean up a comment in plugins/romega/ReflOmegaCoreGravatar Jason Gross2014-08-25
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Correct a spelling mistakeGravatar Jason Gross2014-08-25
* factored out require_modifiers + bug fix.Gravatar Gregory Malecha2014-08-25
* coqdep comments counter is in the stackGravatar Pierre Boutillier2014-08-25
* a comment about the new state.Gravatar Gregory Malecha2014-08-25
* Support for Timeout n and From ..Gravatar Gregory Malecha2014-08-25
* Make coqdep find Require commands prefixed by TimeGravatar Gregory Malecha2014-08-25
* Fixing previous commit.Gravatar Pierre-Marie Pédrot2014-08-25
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
* Removing a unused legacy parsing rule.Gravatar Pierre-Marie Pédrot2014-08-24
* Fixing bug #3404.Gravatar Pierre-Marie Pédrot2014-08-24
* Enabling drag & drop on the source view widgets.Gravatar Pierre-Marie Pédrot2014-08-24
* Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherGravatar Pierre-Marie Pédrot2014-08-23
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-23
* Fixing ml-dot & mli-dot targets.Gravatar Pierre-Marie Pédrot2014-08-23
* Fixing bug #3533.Gravatar Pierre-Marie Pédrot2014-08-23
* Tactics.unify in the new monad.Gravatar Pierre-Marie Pédrot2014-08-23
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a Goal.sensitive in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of tclSENSITIVE in Rewrite.Gravatar Pierre-Marie Pédrot2014-08-21
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Space after [identity] coercion keywords (beautifier).Gravatar Xavier Clerc2014-08-21
* Avoid redundant spaces (beautifier).Gravatar Xavier Clerc2014-08-21
* Do not drop the locality qualifier (beautifier).Gravatar Xavier Clerc2014-08-21
* Make beautify-archive usable on non-GNU systems.Gravatar Xavier Clerc2014-08-21
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
* New primitive allowing to modify refine handles.Gravatar Pierre-Marie Pédrot2014-08-19
* Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger...Gravatar Matthieu Sozeau2014-08-18
* Fixing unification of subterms identified by patterns.Gravatar Hugo Herbelin2014-08-18
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 23:16:39 +0000