aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-08-11SearchAbout and similar: add a customizable blacklistletouzey
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
2011-08-10Fixing typos in commentsherbelin
2011-08-10Improving error message about coinductive guard (old "cases" is now "match")herbelin
2011-08-10Fixing printing bug with last trailing non-maximally implicitherbelin
2011-08-10Exported tactic intro_thenherbelin
2011-08-10Made CHANGES more uniformly writtenherbelin
2011-08-10Take benefit of bullets available by default in Preludeherbelin
2011-08-10Less ambitious application of a notation for eq_rect. We proposedherbelin
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
2011-08-10Fix implementation of Hint Immediate used by typeclasses eautomsozeau
2011-08-10Added list_map_filter_imsozeau
2011-08-10Graceful error message for [Proof Mode] and [Set Default Proof Mode] when req...aspiwack
2011-08-09BinInt: more structured scripts thanks to bullets and { }letouzey
2011-08-09Coqide: revised parsing of coq sentencesletouzey
2011-08-09In coqtop, a terminating "." must now be followed by a blank or eof.letouzey
2011-08-09Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...aspiwack
2011-08-08Some forgotten lemma in Arith with "O" in the name instead of "0".herbelin
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
2011-08-08Two bugs in pattern-matching compilation:herbelin
2011-08-08Term: fix hash_constr to hash modulo casts & names (like compare_constr)puech
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-08-04moins de reification inutile, noatations standardspottier
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-08-03Fix nf_evars_undefined use in pr_constraintsmsozeau
2011-08-03Fix nf_evars_undefinedmsozeau
2011-08-02Patch to simplify is_open_canonical_projectionherbelin
2011-08-02More robust evar_map debugging printerherbelin
2011-08-01Term: simplify compare_constr by removing calls to decompose_apppuech
2011-08-01Added .dir-locals file to take advantage of emacs 23's new Directory-local va...puech
2011-08-01fixed bug 2580. Quick fix: copy emitcodes before patching itbarras
2011-07-29Ring: replaced various generic = on constr by eq_constr, destructors etc.puech
2011-07-29Quote: replaced various generic = on constr by eq_constr, destructors etc.puech
2011-07-29generic = on named_context replaced by named_context_equalpuech
2011-07-29Newring: generic = on constr replaced by eq_constrpuech
2011-07-29Coq_micromega: generic = on constr replaced by eq_constrpuech
2011-07-29Field: generic Gmap on constr replaced by Cmappuech
2011-07-29Extract_env: generic = on prec_declaration replaced by prec_declaration_equalpuech
2011-07-29Tactics: replace generic = on constr by destructorspuech
2011-07-29Auto: replace generic compare on pri_auto_tactic by pri_auto_tactic_ordpuech
2011-07-29Extraction: replace generic = on mutual_inductive_body by mib_equalpuech
2011-07-29Evarutil: replace generic list_distinct on constr by constr_list_distinctpuech
2011-07-29replaced some generic = on constr by eq_constrpuech
2011-07-29Subtac_cases: replaced some generic = on constr by destructorspuech
2011-07-29Ring: replaced some generic Pervasives.compare on constr by constr_ordpuech
2011-07-29Add printer dependency to Hashtbl_alt (used in Term)puech
2011-07-29Nsatz: replaced some generic = on constr by eq_constrpuech
2011-07-29Recdef: replaced some generic = on constr by eq_constrpuech
2011-07-29FourierR: replaced some generic Hashtbl on constr by Constrhashpuech
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:26:25 +0000