aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Fix commentGravatar glondu2010-06-07
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Typo in comment of proof.mlGravatar herbelin2010-05-29
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Fix: Pfedit.get_current_goal_context when no goal is focused.Gravatar aspiwack2010-05-10
* Removed an evar_merge in clenv_fchain which not only is incorrect butGravatar herbelin2010-05-10
* Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofGravatar pboutill2010-05-05
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Consider OccurCheck a catchable exception.Gravatar msozeau2010-03-08
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Attached evar source to the evar_info and add location to tclWITHHOLES errorsGravatar herbelin2009-12-22
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* In "progress", extending the set of evars w/o solving an existing one isGravatar herbelin2009-12-21
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Take constraints into account in the "instantiate" tacticGravatar herbelin2009-10-30
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
* fixed czar bug with parametric inductivesGravatar corbinea2009-10-27
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* - Fixed a bug in checking that implicit arguments are all correctlyGravatar herbelin2009-09-18
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 09:54:07 +0000