aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Add compatibility option "-compat 8.3".Gravatar herbelin2011-06-20
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* Fixing bug #2181 (Class mechanism can create dependencies over unnamedGravatar herbelin2011-06-14
* Another bug of Scheme Induction (generated names dep/nodep were swapped).Gravatar herbelin2011-06-13
* Fixing an anomaly in Scheme Induction.Gravatar herbelin2011-06-13
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
* Coqide: allow the use of Abort (grant wish #2357)Gravatar letouzey2011-05-18
* More work on error handlingGravatar letouzey2011-05-17
* Break circular dependency Proof_global -> Vernacexpr -> Proof_global.Gravatar aspiwack2011-05-17
* Repair the "Fail" command after recent changes in exception handlingGravatar letouzey2011-05-16
* turn the automatic generation of boolean equalityGravatar vsiles2011-05-16
* Turning Sys_error into error by default instead of anomaly. After all,Gravatar herbelin2011-05-15
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* New option [Set Bullet Behavior] allows to select the behaviour of bullets.Gravatar aspiwack2011-05-13
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
* Fixed a bug causing inconsistent states during proof editting.Gravatar aspiwack2011-04-29
* coqtop -config returns coq returns coq environments at exection timeGravatar pboutill2011-04-28
* Fixed notation printing bug when curly brackets are involved (requestsGravatar herbelin2011-04-28
* Coqide: better handling of stdout/stderr in win32Gravatar letouzey2011-04-21
* Add a flag to control betaiota reduction during unification to maintain backw...Gravatar msozeau2011-04-18
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
* Reorder search path order, so the standard library is search last.Gravatar herbelin2011-04-14
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
* Fixed "Eval ... in t" when t has still metavariables.Gravatar herbelin2011-04-08
* Add 'Existing Instances' declaration to declare multiple instances at once.Gravatar letouzey2011-04-06
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Ide_intf: documentation of calls + debug printing of calls/answersGravatar letouzey2011-03-30
* Ide_intf: remove useless int answer to the "interp" and "rewind" callsGravatar letouzey2011-03-30
* Ide_slave: better handling of Ctrl-CGravatar letouzey2011-03-30
* Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakGravatar letouzey2011-03-28
* Ide_slave: improved handling of exceptions (in particular ^C)Gravatar letouzey2011-03-28
* Ide_slave: a more robust current_status () functionGravatar letouzey2011-03-28
* Ide_intf : change type of location in ideGravatar letouzey2011-03-25
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
* Ide: experimentally allow coqide to interrupt or kill coqtopGravatar letouzey2011-03-23
* - Fix solve_simpl_eqn which was cheking instances types in the wrong environm...Gravatar msozeau2011-03-23
* An option "Set Default Timeout n."Gravatar letouzey2011-03-17
* Goptions: repair Unset for int optionsGravatar letouzey2011-03-17
* Finish branching functions handling module errors (cf. r13886)Gravatar letouzey2011-03-16
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07