aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-03-31A more reasonable implementation of Loadpath.Pierre-Marie Pédrot
2015-03-31Declarative mode: fix proof modes.Arnaud Spiwack
2015-03-31Declarative mode: fix vernac classification.Arnaud Spiwack
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
2015-03-31Better formatting of messages in proofs.Arnaud Spiwack
2015-03-31Generalisation of the "end command" argument of the goal printer.Arnaud Spiwack
2015-03-31Fix various typos in documentationMatěj Grabovský
2015-03-31Do not escape "'" when outputting to html, especially not using "´".Guillaume Melquiond
2015-03-30grammar: export constr_evalEnrico Tassi
2015-03-30grammar: export hypidentEnrico Tassi
2015-03-30camlp4: grep away warnings in output/* testsEnrico Tassi
2015-03-30coq_makefile: fix compilation with camlp4Enrico Tassi
2015-03-30fix code and bound for SWITCH instruction.Benjamin Gregoire
2015-03-29Ensuring more invariants in Constr_matching.Pierre-Marie Pédrot
2015-03-29Adding test for bug #4165.Pierre-Marie Pédrot
2015-03-29Fixing bug #4165.Pierre-Marie Pédrot
2015-03-27Normalize scope names before storing them in vo files. (Fix for bug #4162)Guillaume Melquiond
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-27STM: refine the notion of "simply a tactic"Enrico Tassi
2015-03-27Properly handle extra "clean" targets with coq_makefile.Guillaume Melquiond
2015-03-27use a more compact representation of non-constant constructorsBenjamin Gregoire
2015-03-26allows the vm to deal with inductive type with 8388607 constant constructors ...Benjamin Gregoire
2015-03-26fix compilationBenjamin Gregoire
2015-03-26Fix bug 4157,Benjamin Gregoire
2015-03-26add coqdep in distributed_exec, else make does not work.Benjamin Gregoire
2015-03-26STM: change how proof mode switching commands are handled (decl_mode)Enrico Tassi
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-03-25More clever representation of substituted Cemitcode.Pierre-Marie Pédrot
2015-03-25Summary: fix code to detect functional values in summaryEnrico Tassi
2015-03-25STM: avoid processing asynchronously empty proofs (Close: #4134)Enrico Tassi
2015-03-25Exporting memory representation of STM tasks for votour.Pierre-Marie Pédrot
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-03-25Another example about the consequence of a wrong computation of theHugo Herbelin
2015-03-25Use kernel names instead of user names when looking for coercions. (Fix for b...Guillaume Melquiond
2015-03-25coqc: fix --helpEnrico Tassi
2015-03-25Correcting a bug introduced by universes polymorphismjforest
2015-03-25correcting a bug with aliased when using Functional Schemeforest
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
2015-03-24Fixing computation of non-recursively uniform arguments in theHugo Herbelin
2015-03-24Fixing wrong rel_context in checking positivity condition.Hugo Herbelin
2015-03-24Functorized interface over object representation in votour.Pierre-Marie Pédrot
2015-03-24Fixing representation of dynamics in votour (again).Pierre-Marie Pédrot
2015-03-24Fixing equality of notation_constrs. Fixes bug #4136.Pierre-Marie Pédrot
2015-03-24Revert "Useless check when loading notations through import."Pierre-Marie Pédrot
2015-03-23Dedicated type for on-demand objects in Library.Pierre-Marie Pédrot
2015-03-23coqchk: more prints when -debugEnrico Tassi
2015-03-23Load: don't give anomaly on aborted proofs (Close: #3882)Enrico Tassi
2015-03-22Announcing * and ** which were not official yet in 8.4.Hugo Herbelin
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-03-22Aliasing give_up with admitEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 07:10:21 +0000