index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
miscops.ml
Age
Commit message (
Expand
)
Author
2018-06-12
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-05-31
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-08
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-03-09
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-01
Proper nametab handling of global universe names
Matthieu Sozeau
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-03
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-04-24
[location] Use located in misctypes.
Emilio Jesus Gallego Arias
2017-02-14
Clenv API using EConstr.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-10-07
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-07-21
Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-12
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-11-21
Avoid compilation warning.
Matthieu Sozeau
2014-11-19
Making map_union a standard function of the ML library.
Hugo Herbelin
2014-11-16
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-09-30
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-08
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-03-02
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2013-07-09
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-01-22
New implementation of the conversion test, using normalization by evaluation to
mdenes
2012-08-08
Updating headers.
herbelin
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
