aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/redexpr.ml
Commit message (Expand)AuthorAge
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantGravatar herbelin2007-04-13
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Adoption du nom canonique global_of_constr pour éviter confusion avec type r...Gravatar herbelin2005-05-20
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02