aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* - Rebranchement backtrack du langage déclaratif dans CoqideGravatar herbelin2008-07-18
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Changement de catch_error pour qu'il rattrape les erreurs d'arguments Gravatar aspiwack2008-06-27
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* fixed catch_failerror + improved progress check + fixed repeat (repeat simpl ...Gravatar barras2008-05-29
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Suite commit 10861Gravatar herbelin2008-04-28
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* Diverses corrections Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Solde de code mort et petites optimisations sur lesquels je suisGravatar herbelin2008-02-09
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Adding the tactic "instantiate" (without argument), to force theGravatar glondu2007-12-07
* Util.option_compare devient Option.Misc.Compare et change un peu de type Gravatar aspiwack2007-12-07
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Enlevé les trucs commités au mauvais endroitGravatar aspiwack2007-10-23
* Quelques structures de donnée plus les modules principaux (et Gravatar aspiwack2007-10-23
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
* Declarative language: fixed the generation of fixpoints for induction proofs.Gravatar corbinea2007-07-24
* (Port of r9984) Easier debugging:Gravatar glondu2007-07-12
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06