index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
evarconv.mli
Commit message (
Expand
)
Author
Age
*
Reductionops.Stack.strip* are ready to deal with Shift
Pierre Boutillier
2014-02-24
*
Stack operations of Reductionops in Reductionops.Stack
Pierre Boutillier
2014-02-24
*
comments in mli
pboutill
2013-05-30
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
A few comments in evarconv.mli.
herbelin
2013-05-09
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...
pboutill
2013-02-25
*
A more informative message when the elimination predicate for
herbelin
2013-02-17
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Unification in Evar_conv uses an abstract machine state
pboutill
2012-08-09
*
Updating headers.
herbelin
2012-08-08
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Refined second_order_matching so that a constraint on which
herbelin
2011-11-08
*
Completing r14538 (Chung-Kil Hur's trick for fast dependently-typed
herbelin
2011-10-11
*
Applied the trick of Chung-Kil Hur to solve second-order matching
herbelin
2011-10-10
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
*
- Use transparency information all the way through unification and
msozeau
2011-02-17
*
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
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Fix treatment of remaining unification constraints: raise a more
msozeau
2010-03-07
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Backtrack on experimental unification with sort variables: it requires
msozeau
2009-06-02
*
Populate the sort constraints set correctly during unification. Add a
msozeau
2009-05-27
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
(Tentative to) add Canonical Structure resolution to the regular
msozeau
2009-05-16
*
Report de l'heuristique d'unification premier ordre flexible/rigide
herbelin
2006-09-15
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
Nouvelle en-tĂȘte
herbelin
2004-07-16
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
entetes
filliatr
2001-03-15
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Petit nettoyage de Evarutil et Evarconv
herbelin
2000-10-23
*
documentation
filliatr
2000-01-28
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
- environment -> safe_environment
filliatr
1999-12-01
*
portage modules Evarconv et Evarutil
filliatr
1999-11-29
*
Versions initiales
herbelin
1999-11-24
*
organisation de trad (entre parsing/ et pretyping/)
filliatr
1999-10-13