aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/record.ml
Commit message (Expand)AuthorAge
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Disable debug printingGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Fix bugsGravatar Amin Timany2017-06-16
* Subtyping inference for inductoves and recordsGravatar Amin Timany2017-06-16
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
* Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| * More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
| * Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
| * Using EConstr and more invariants in record.ml.Gravatar Hugo Herbelin2017-05-31
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| |
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| * | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ /
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15