index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
patternops.ml
Commit message (
Expand
)
Author
Age
*
Tactic_matching API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Cleaning up opening of the EConstr module in pretyping folder.
Pierre-Marie Pédrot
2017-02-14
*
Patternops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
*
Fixing non exhaustive pattern-matching.
Hugo Herbelin
2015-04-22
*
Fixing #3383 (a "return" clause without an "in" clause is not enough
Hugo Herbelin
2015-04-21
*
Really fix constr_of_pattern and bugs #3590 and #4120 by
Matthieu Sozeau
2015-04-09
*
Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...
Matthieu Sozeau
2015-04-09
*
Fix bug #3590, keeping evars that are not turned into named metas by
Matthieu Sozeau
2015-03-03
*
Update headers.
Maxime Dénès
2015-01-12
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Fixing #3623 (unbound evars in types in a call to "change with").
Hugo Herbelin
2014-10-03
*
Completing fixing order of parameters when translating from
Hugo Herbelin
2014-10-02
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Make pattern_of_constr typed so that we can infer the proper patterns
Matthieu Sozeau
2014-09-27
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Move the specific map_constr_with_binders_left_to_right
Matthieu Sozeau
2014-09-19
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
2014-09-15
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
cList.index is now cList.index_f, same for index0
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Fixing #3088. Translation from globconstrs to patterns was forgetting
ppedrot
2013-08-01
*
Replacing lists by maps in matching interpretation.
ppedrot
2013-06-05
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Renamed Option.Misc.compare to the more uniform Option.equal.
ppedrot
2012-12-13
*
Added a constr_pattern_eq
ppedrot
2012-11-23
*
Monomorphization (pretyping)
ppedrot
2012-11-22
[next]