index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
/
indfun.ml
Commit message (
Expand
)
Author
Age
*
A uniformization step around understand_* and interp_* functions.
herbelin
2013-05-09
*
Indfun : use States.with_state_protection instead of freeze/unfreeze
letouzey
2013-04-23
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 7)
letouzey
2013-03-13
*
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Taking into account the type of a definition (if it exists), and the
herbelin
2012-11-17
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
Final part of moving Program code inside the main code. Adapted add_definitio...
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
New version of recdef :
jforest
2012-03-01
*
In the syntax of pattern matching, "in" clauses are patterns.
pboutill
2012-02-29
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Call process_vernac_interp_error before calling Errors.print in
herbelin
2011-06-10
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Rename files in funind to respect new conventions
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Report fix bug 2345 from v8.3 (Bad error message when functional
courtieu
2010-09-21
*
correcting a bug in funind introduced in r 13292
jforest
2010-07-23
*
Simplified the way internalization_data (i.e. bindings of bound vars
herbelin
2010-07-22
*
Amelioration dans Function
jforest
2010-07-16
*
Fixed commit 13125 (stricter check of induction args): an interpretation
herbelin
2010-06-14
*
Allowing to use an ordering different than Lt with measure
jforest
2010-06-09
*
Using vernac parsing for Function
jforest
2010-06-08
[next]