aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-06-13Fixing an anomaly in Scheme Induction.herbelin
2011-06-12Oups, typo in previous commitherbelin
2011-06-12Removed what looks like a (very old) useless f.o. unification passherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-12Rather quick hack to avoid using notations involving "Type" whenherbelin
2011-06-11Coqide now need lablgtk2.14.0pboutill
2011-06-10Updated CHANGES (info, Show Script, rephrasing).herbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-06-10Fixing the "buggy" first_name and prepare multi-induction.herbelin
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
2011-06-10Integrating onLastHypId into intro so that we can get the introductionherbelin
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
2011-06-10Coqide Menubar integration in MacOSpboutill
2011-06-10no more errors at _stubs.c.d generationpboutill
2011-06-10Menubar and toolbar in coqide using GtkUI & Gactions.pboutill
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing constrai...msozeau
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:44:33 +0000