aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-03-21Documentation of the timeout tactical (cf r13917)letouzey
2011-03-21Init: some results in Type should rather be Defined than Qedletouzey
2011-03-21Makefile.build: states/initial.coq was wrongly done with -dont-load-proofsletouzey
2011-03-18Makefile.build: compile the stdlib with -dont-load-proofs by defaultletouzey
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-03-17An option "Set Default Timeout n."letouzey
2011-03-17Goptions: repair Unset for int optionsletouzey
2011-03-17CompareSpec: a slight generalization/reformulation of CompSpecletouzey
2011-03-16Adapt printers.mllib after my last commitletouzey
2011-03-16Finish branching functions handling module errors (cf. r13886)letouzey
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2011-03-16Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionletouzey
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
2011-03-11Inference of match predicate produces ill-typed unification problem,msozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-11- Better error messages taking unif. constraints into account.msozeau
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-03-10Do not forget conv_pbs when resetting an evm: msozeau
2011-03-10ZBits,ZdivEucl,ZDivFloor: a few lemmas with weaker preconditionsletouzey
2011-03-08Solve evar instantiations in the right environment.msozeau
2011-03-08Fix declarations of [Add Setoid/Morphism...] in sections to not exportmsozeau
2011-03-08syntax for exponentspottier
2011-03-08adding eta in the vmbgregoir
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-07CHANGES: mentionning quickly Separate Extractionletouzey
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
2011-03-07Extraction: fix printing of haskell modular namesletouzey
2011-03-07Extraction: avoid printing unused mutual fix components (fix #2477)letouzey
2011-03-07A new command "Separate Extraction"letouzey
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2011-03-05A few more betaiota on environments and types of error messages. Seems toherbelin
2011-03-05Added support for instantiation of ?n by a lambda when "?n a" has toherbelin
2011-03-05Reorganized a bit evarconv.ml:herbelin
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-03-05Instantiate evar by a lambda when "?n args" has to unify with Prodherbelin
2011-03-05Fixed a "feature" about subtyping records: one was expected not onlyherbelin
2011-03-05Restore documentation of library String which was removed in 2007 (r10049)herbelin
2011-03-05Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notationherbelin
2011-03-05Fixing injection bug #2493 (regression introduced by fixing injectionherbelin
2011-03-04CHANGES: update of syntax for annotations of functor applicationletouzey
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-03-04Simplify proofs in Permutation using generalized rewriting.msozeau
2011-03-04- Allow to set a particular transparent_state for the local hintmsozeau
2011-03-04checker: cleanupglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 07:22:08 +0000