aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-01-22- Fix evarconv so that we have complete eta-conversion:msozeau
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
2013-01-21Last test-suite not in Symmetric Patterns syntaxpboutill
2013-01-18I forget to use git log before git svn dcommit ...pboutill
2013-01-18Evarconv: Check stack before term in Canonical Structure approuvalpboutill
2013-01-18Unset Asymmetric Patternspboutill
2013-01-18Revert "coq_makefile: use coqdep instead of ocamldep on .ml4 files"pboutill
2013-01-12Envar: in w32, add .exe when searching for caml binariesletouzey
2013-01-12Coqmktop and camlp4 : sequel to commit 16113letouzey
2013-01-07Coq_makefile: quoting pathspboutill
2013-01-07Coq_makefile: -extra & -phony-extra for user defined makefile rulepboutill
2013-01-07Fixup notation printing in patternspboutill
2013-01-06* Kernel/Terms:regisgia
2012-12-22Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.herbelin
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
2012-12-21Fixup and comment reductionopspboutill
2012-12-19Reductionops reduction machine can refold constantpboutill
2012-12-19Evarconv.Pseudorigid erasurepboutill
2012-12-19Coqide: cleaner Coq.PrintOpt and session creationletouzey
2012-12-19Array.create is deprecatedpboutill
2012-12-19GtkData.set_default_modifiers and no access to <primary> in lablgtk -> unsuab...pboutill
2012-12-19Fix coqtop -config when absolute path have been given for ocaml*pboutill
2012-12-18Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)letouzey
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-12-18Extraction: qualified names in Extract Constant examples (fix #2878)letouzey
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-18Factorization of the elim unif flag with the default flag. Sinceherbelin
2012-12-17Fixed interpretation of "x" as a binding variable for the returnherbelin
2012-12-17Do not display REVERTcast inserted by reduction tactics (unless printing all).herbelin
2012-12-17Fixed a bug in the algorithm trying to elaborate a "match" return predicate.herbelin
2012-12-17Ide_slave: do not prepare debug messages in non-debug modeletouzey
2012-12-17Extraction of projections: restrict a hack to ocaml only (fix #2941)letouzey
2012-12-14Fixing ocalmdoc commentppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Fixing CoqIDE compilationppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Documented CString.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 13:27:29 +0000