aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-01-27Improving formatting of output of "Test table".herbelin
2013-01-27Fixed bug #2967 (some missing check on ill-formed recursive notation strings).herbelin
2013-01-27Slightly improving some debugging printing and error message for modules.herbelin
2013-01-27Avoid failure in debugger when printing Ltac names.herbelin
2013-01-26updating ide/coq documentationppedrot
2013-01-26Monadification of coqtop queries in CoqIDEppedrot
2013-01-26Uniformization of Coq tasksppedrot
2013-01-25Better handling of escape find in CoqIDEppedrot
2013-01-25Better Undo/Redo mechanismppedrot
2013-01-25Trying to fix CoqIDE undo/redo mechanismppedrot
2013-01-25Fixing autocompletion in CoqIDEppedrot
2013-01-25Fixup last commitppedrot
2013-01-25Hugo request: CoqIDE find on enterppedrot
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
2013-01-24Fixed parsing of -no-native-compiler flag.mdenes
2013-01-24Native compiler: warnings were not turned off for OCaml 3.11mdenes
2013-01-23Coqide: limit read buffer size to 4096 (pipe size in win32)letouzey
2013-01-22Coqide: avoid potentially blocking read on coqtop channelletouzey
2013-01-22Added .native to .gitignoreppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-22Revert "remove -rectypes except for term.ml"mdenes
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:52:49 +0000