aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:46:10 +0000