aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
2011-06-08Make Notation works with anonymous-level "Type".herbelin
2011-06-08Fixes in pruning in unification.msozeau
2011-06-07Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...msozeau
2011-06-07Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...msozeau
2011-06-07Catch AbstractionOverMeta as a unification failure in precatchable_exception.msozeau
2011-06-07Fix bug #2415: warn when closing modules or sections and some obligations are...msozeau
2011-06-07Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.msozeau
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to typechec...msozeau
2011-06-06Typo.gmelquio
2011-05-26Mini-test for etaherbelin
2011-05-26Partial fix for accepting bound variables with same name as implicitherbelin
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-05-25Q2R -> IQRfbesson
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-24Applying Enrico Tassi's patch for giving priority to delta over eta inherbelin
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-23ported r14149 from v8.3 branch: bug in checker (redefined global)barras
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
2011-05-20added support to handle division by a constant over Rfbesson
2011-05-19Remove useless "open Gc"glondu
2011-05-19Remove System.process_time (dead code)glondu
2011-05-19Extraction: avoid lots of late mind_of_knletouzey
2011-05-19Extraction: global reference should be indexed on their user part (fix #2540)letouzey
2011-05-18cbv delta - [...] before calling liafbesson
2011-05-18apply zeta reduction before syntaxificationfbesson
2011-05-18Extraction: avoid printing of Recursive Extraction in coqide's consoleletouzey
2011-05-18Coqide: allow the use of Abort (grant wish #2357)letouzey
2011-05-17Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)letouzey
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-05-17More work on error handlingletouzey
2011-05-17Add simple test of bullet behaviour.aspiwack
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-17Fixes bug in [maximal_unfocus] introduced in r14120.aspiwack
2011-05-16Repair the "Fail" command after recent changes in exception handlingletouzey
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
2011-05-16Fix order in Search tests.letouzey
2011-05-16Fixed my last patch: these files no longer use nat_beq (automaticallyvsiles
2011-05-16turn the automatic generation of boolean equalityvsiles
2011-05-15Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).herbelin
2011-05-15Failing instead of switching to the coercion mechanism when VMcastherbelin
2011-05-15Turning Sys_error into error by default instead of anomaly. After all,herbelin
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
2011-05-13The modules in proofs now use the Errors module to explain their exceptions t...aspiwack
2011-05-13A new mechanism to handle errors.aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-05-09Improved lia + experimental nliafbesson
2011-05-09remove useless dependancy for csdpcertfbesson
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 23:52:57 +0000