aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \
| * | Adding a test file for evar handling in the VM.Gravatar Pierre-Marie Pédrot2018-03-03
* | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
|/ /
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
* Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\
| * Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
* | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ | |/ |/|
| * More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| * Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
* | Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
|/
* Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Gravatar Maxime Dénès2017-12-18
|\
* | Fix anomaly in [Type foo] command, + print uctx like Check.Gravatar Gaëtan Gilbert2017-12-11
| * use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
|/
* Tests for global universe declarationsGravatar Matthieu Sozeau2017-12-01
* Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Gravatar Maxime Dénès2017-11-30
|\
* \ Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Gravatar Maxime Dénès2017-11-29
|\ \
| | * Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |/ |/|
| * Fixing associativity registered for level 10.Gravatar Hugo Herbelin2017-11-27
* | Restrict universe context when declaring constants in obligations.Gravatar Gaëtan Gilbert2017-11-25
* | Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
* | In close_proof only check univ decls with the restricted context.Gravatar Gaëtan Gilbert2017-11-24
* | restrict_universe_context: do not prune named universes.Gravatar Gaëtan Gilbert2017-11-24
* | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
|/
* Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
* Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Gravatar Maxime Dénès2017-11-20
|\
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
* | Merge PR #922: New beta-iota compatibility refinementsGravatar Maxime Dénès2017-11-08
|\ \ | |/ |/|
* | Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \
| * | Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
* | | Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
* | | Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\ \ \
* | | | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |/ / |/| |
| * | romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
|/ /
* | Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...Gravatar Maxime Dénès2017-10-05
|\ \
* | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| * | Fixing an old bug in collecting evars with cleared context.Gravatar Hugo Herbelin2017-09-27
|/ /
* | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \
* | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| * | test-suite: polymorphismGravatar Matthieu Sozeau2017-09-19
| * | Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
| * | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* | | Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ \ | |/ / |/| |
| * | Add test-suite script by Cyprien ManginGravatar Matthieu Sozeau2017-09-18
* | | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Gravatar Maxime Dénès2017-09-15
|\ \ \