aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Expand)AuthorAge
* Test files for subtac.Gravatar msozeau2006-04-14
* Simplifying the proof of principlesGravatar jforest2006-04-12
* Fixes for new unification, not used in default version as it really changes u...Gravatar msozeau2006-04-10
* + Changing a little functional schemes types Gravatar jforest2006-04-10
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...Gravatar msozeau2006-04-10
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* appel Zenon sans preludeGravatar filliatr2006-03-27
* utilisation de la VM pour la normalisation finale de romegaGravatar letouzey2006-03-24
* correctifs de bug pour romega: Gravatar letouzey2006-03-23
* Subtac fixes, single fixpoint definitions are working again. Added a toggle o...Gravatar msozeau2006-03-22
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* Adding "New Functional Scheme" Gravatar jforest2006-03-20
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
* Cleaning dead code Gravatar jforest2006-03-16
* + Debugging and cleaning functional principle generation tacticGravatar jforest2006-03-14
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* -Debugging multiple induction, a bug appeared when having functionGravatar courtieu2006-03-12
* cleaning Gravatar jforest2006-03-10
* Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...Gravatar jforest2006-03-07
* Exploitation du 'let rec' + présentationGravatar herbelin2006-03-05
* New files for subtacGravatar coq2006-03-05
* tactic haRVey pour appeler haRVey (contrib/dp)Gravatar filliatr2006-03-02
* Correction bug #842 (rename d'une hyp du contexte)Gravatar herbelin2006-03-01
* appel de ZenonGravatar filliatr2006-03-01
* *** empty log message ***Gravatar filliatr2006-02-28
* dp: sortie WhyGravatar filliatr2006-02-27
* Work on recursive definitionsGravatar coq2006-02-22
* Add vernacular file for subtacGravatar coq2006-02-22
* Julien:Gravatar bertot2006-02-22
* Work with binder lists, problem of tyconsGravatar coq2006-02-21
* Latest fixes, should work fine now for non recursive definitions, although st...Gravatar coq2006-02-21
* Fix minor bugGravatar coq2006-02-20
* Forgot a fileGravatar coq2006-02-20
* Monday work, working with coercions and implicit argsGravatar coq2006-02-20
* Forgot another file...Gravatar coq2006-02-20
* Forgot one fileGravatar coq2006-02-20
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20
* bug correctionGravatar bertot2006-02-17
* Julien:Gravatar bertot2006-02-17
* changed the decomposition of an induction schemeGravatar coq2006-02-17
* firstorder fails gracefullly when encountering untypable higher-order termsGravatar corbinea2006-02-13
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* very minor bug correction and cleanningGravatar bertot2006-02-09
* securing intros (we now use h_intro)Gravatar bertot2006-02-09
* Minor bugs fixesGravatar bertot2006-02-09
* Changing Set to Type for iter.Gravatar bertot2006-02-08
* One can use a measure {mes f x} instead of a well-founded relation in GenFixp...Gravatar bertot2006-02-08
* Julien:Gravatar bertot2006-02-08
* added mli 's for the nex functional induction (forgotten last time).Gravatar coq2006-02-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 17:06:32 +0000