aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-03-28Ide: new option -coqtop <mycoqtop> + remove wrong quoting of argsletouzey
2011-03-25ide/coqide.ml: a pass of more decent automatic indentationletouzey
2011-03-25Ide: more reorganisation and cleanupletouzey
2011-03-25Ide_intf : change type of location in ideletouzey
2011-03-25Ide: mention "Restart" instead of "Go to start" for corresponding buttonletouzey
2011-03-23Ide: stronger separation from coqtopletouzey
2011-03-23Ide: experimentally allow coqide to interrupt or kill coqtopletouzey
2011-03-23- Remove useless grammar rulemsozeau
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 22:38:51 +0000