index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
refine.ml
Age
Commit message (
Expand
)
Author
2003-10-13
Deplacement next_global_ident_away dans Termops
herbelin
2003-05-19
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2002-12-09
Ajout Simpl et Change sur des sous-termes
herbelin
2002-05-29
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-04-02
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-03-27
Simplification de Proof_type.prim_rule
herbelin
2002-02-15
petits changements cosmetiques sur les tactiques
barras
2001-12-18
coq-bugs #12: probleme de metamap resolu
barras
2001-12-13
compat ocaml 3.03
filliatr
2001-11-05
GROS COMMIT:
barras
2001-09-20
let-in dans Refine
filliatr
2001-06-25
Refine sur les CoFix
filliatr
2001-05-25
Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_types
herbelin
2001-05-03
Changement de la structure des points fixes
barras
2001-03-28
amelioration de la structure des univers
barras
2001-03-15
entetes
filliatr
2001-03-09
bug de refine: uncaught exception Array.sub
barras
2001-03-01
nouvelle implantation de la reduction
barras
2000-12-15
suppression warning et calcule type dans replace_by_meta dans tous les cas
filliatr
2000-11-02
suppression des (* open Generic *)
filliatr
2000-10-18
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
Renommage canonique :
herbelin
2000-10-03
mise en page
herbelin
2000-10-01
Renommage AppL en App
herbelin
2000-09-26
Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...
herbelin
2000-09-14
Abstraction de constr
herbelin
2000-09-12
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-10
Correction pour make doc
herbelin
2000-09-10
Suppression de Abst
herbelin
2000-09-10
Ajout d'un LetIn primitif.
herbelin
2000-08-28
cosmétique
herbelin
2000-07-24
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-20
portage Refine
filliatr
[prev]