index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
tacred.mli
Commit message (
Expand
)
Author
Age
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Moved code for finding subterms (pattern, induction, set, generalize, ...)
Hugo Herbelin
2014-06-28
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Simpl_behaviour becomes Reductionops.ReductionBehaviour
Pierre Boutillier
2014-02-24
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-12-18
*
Configurable simpl tactic
gareuselesinge
2011-11-21
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Remove old compatibility stuff (Tacred.nf)
glondu
2009-10-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant
herbelin
2007-04-13
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Amélioration des messages d'erreurs de tacred; unfold considère maintenant le
herbelin
2006-02-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
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
Bug (destruct/induction ne savent pas traiter le cas non atomique avec paramÃ...
herbelin
2004-01-27
*
Bug introduit avec le 'Simpl f'
herbelin
2003-11-22
*
Ajout reduce_to_quantified_ref
herbelin
2003-11-09
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Mise au point de declare_red_expr
herbelin
2002-05-30
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Nettoyage reduce_to_ind et one_step_reduce
herbelin
2001-09-09
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
entetes
filliatr
2001-03-15
*
Mise en place de la possibilite d'unfolder des variables locales et des const...
filliatr
2001-01-31
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Minor correction for Ocamlweb + doc update
coq
2000-09-14
*
Déplacement de fonctions de Reduction vers Tacred
herbelin
2000-09-14
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
*
- états fabriqués avec -silent
filliatr
1999-12-13
*
modifs pour premiere edition de liens
filliatr
1999-12-02