index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tactics.mli
Commit message (
Expand
)
Author
Age
...
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Essai de partage de code entre apply et eapply
herbelin
2007-04-15
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Ajout de la tactique "apply in".
herbelin
2006-10-24
*
Correction du bug #1116
jforest
2006-07-20
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
adding a new tactic [intro_avoiding idl] which acts as intro but prevents the
jforest
2006-04-11
*
+ destruct now works as induction on multiple arguments :
jforest
2006-03-21
*
-Debugging multiple induction, a bug appeared when having function
courtieu
2006-03-12
*
changed the decomposition of an induction scheme
coq
2006-02-17
*
added isProd to term.mli.
coq
2006-02-16
*
induction now admits multiple induction arguments. The principle must
coq
2006-02-10
*
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
herbelin
2006-01-16
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Ajout de l'axiome du but prouve par la tactique simplifi
coq
2005-03-22
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
Restructuration fonctions de réécriture depuis égalité dépendante; facto...
herbelin
2004-10-27
*
reflexivity, symmetry, symmetry ... in e transitivity now fall-back
sacerdot
2004-10-14
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
unification encore...
barras
2004-09-08
*
Nouvelle en-tête
herbelin
2004-07-16
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Correction sur commit précédent : Tactics.cut réduisait de manière inappr...
herbelin
2004-03-01
*
Déplacement définition intro_pattern_expr dans Genarg
herbelin
2004-03-01
*
bugs avec Pose et Assert
barras
2004-01-09
*
Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...
herbelin
2003-11-25
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Deplacement next_global_ident_away dans Termops
herbelin
2003-10-13
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Un type "standardisé" pour new_hyp
herbelin
2003-01-25
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
Uniformisation convert_hyp; correction problème de dépendance dans letin_tac
herbelin
2002-02-28
[prev]
[next]