index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrexpr_ops.ml
Age
Commit message (
Expand
)
Author
2017-06-14
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
Pierre Letouzey
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-15
[interp] [ast] Make raw_cases_pattern_expr private.
Emilio Jesus Gallego Arias
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] More located use.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-12
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-03-24
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
"Standardizing" the name LocalPatten into LocalRawPattern.
Hugo Herbelin
2017-03-23
Factorizing/unifying code in dealing with binders.
Hugo Herbelin
2017-03-23
Improving the API of constrexpr_ops.mli.
Hugo Herbelin
2016-09-22
Revert "Merge remote-tracking branch 'github/pr/283' into trunk"
Maxime Dénès
2016-09-20
Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.
Maxime Dénès
2016-08-19
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-27
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-03-13
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: removing unused field
Matej Kosik
2015-12-18
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-01-12
Update headers.
Maxime Dénès
2014-09-30
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-12
Parsing evar instances.
Hugo Herbelin
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-03-02
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2013-11-27
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-09-18
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2012-12-18
Modulification of name
ppedrot
2012-12-18
Fixing parsing of specific primitive tokens used as notations for patterns
herbelin
2012-12-14
Modulification of identifier
ppedrot
2012-12-14
Implemented a full-fledged equality on [constr_expr]. By the way,
ppedrot
2012-11-25
More equality functions
ppedrot
2012-11-13
More monomorphizations
ppedrot
2012-09-14
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-08-08
Updating headers.
herbelin
2012-06-22
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-14
Internalization of pattern is done in two phases.
pboutill
2012-05-29
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
