aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-11-30Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...ppedrot
2011-11-30Continuing r14747 being actually incomplete (flushing warnings andherbelin
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
2011-11-30Preventing Implicit Arguments warning to be shown in non verbose modeherbelin
2011-11-29Documentation of appcontextletouzey
2011-11-29Fixed a warning about unused variable introduced in r14731ppedrot
2011-11-29lib/xml_lexer.ml in .gitignore (produced by a .mll)letouzey
2011-11-29Extraction: typo in last commitletouzey
2011-11-29fix for bug #2649corbinea
2011-11-29Term: properly ignore Casts between Apps in constr_ordpuech
2011-11-29Term: useless conversion to list in constr_ord deletedpuech
2011-11-28Finally used typing to decide whether an alias needs to be expanded orherbelin
2011-11-28Fixing dependencies postprocessing bug in pattern-matching compilation.herbelin
2011-11-28Term: Fix hash_constr behavior for Cast lnterleaved in application spines.puech
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-28doc: two minor fixes to make my latex happyletouzey
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-25Added an API call to retrieve and change the option stateppedrot
2011-11-25Separated the toplevel interface into a purely declarative module with associ...ppedrot
2011-11-25Cleaning up XML parsingppedrot
2011-11-25avoid relying on weak invariant in cbv.mlbgregoir
2011-11-24Added a function to inspect current option state.ppedrot
2011-11-24Fixed the XML parser CDATA handling (and changed the EOL convention of these ...ppedrot
2011-11-24Fixed some missing options from previous commit.ppedrot
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-24Moving XML handling to lib directoryppedrot
2011-11-24Correct direction for definitional typeclassesmsozeau
2011-11-23In emacs mode, prints a list of the dependent existential variables introducedaspiwack
2011-11-23Adds a pair of function in Evar_util to gather dependent evars in anaspiwack
2011-11-21Renamig support added to "Arguments"gareuselesinge
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21coqide default pref files are by default in /etc/xdg/coq/pboutill
2011-11-21/home/pirbo/.coqrc* are read againpboutill
2011-11-21-user option removalpboutill
2011-11-21Updated CHANGES file wrt to pattern-matching compilation.herbelin
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Add matching on non-inductive types in building an inversion problemherbelin
2011-11-21Old naming bug in pattern-matching compilation: names in theherbelin
2011-11-21Inlining let-in (i.e. trace of aliases) in extract_predicate for whatherbelin
2011-11-21VectorDef.v takes benefit of dependencies being taken into accountherbelin
2011-11-21In pattern-matching compilation, now taking into account the dependenciesherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
2011-11-21Simplifying history management in pattern-matching compilation.herbelin
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Removing stuff about alias dependencies now become useless.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Updating Cases.v test.herbelin
2011-11-21Dead code + refreshing some comments in cases.ml.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:04:53 +0000