aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-15More tests on brackets with goal selectors (including failures).Théo Zimmermann
2018-01-15Add test-suite file for bracket with goal selector.Théo Zimmermann
2018-01-11Force polymorphic definitions to have no internal constraints.Pierre-Marie Pédrot
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Maxime Dénès
2017-12-11Fix anomaly in [Type foo] command, + print uctx like Check.Gaëtan Gilbert
2017-12-05use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguagePaul Steckler
2017-12-01Tests for global universe declarationsMatthieu Sozeau
2017-11-30Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...Maxime Dénès
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...Maxime Dénès
2017-11-28Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gaëtan Gilbert
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
2017-11-25Restrict universe context when declaring constants in obligations.Gaëtan Gilbert
2017-11-25Fix interpretation of global universes in univdecl constraints.Gaëtan Gilbert
2017-11-24In close_proof only check univ decls with the restricted context.Gaëtan Gilbert
2017-11-24restrict_universe_context: do not prune named universes.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-20Fixing factorization of recursive notations in the case of an atomic separator.Hugo Herbelin
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Maxime Dénès
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
2017-10-05Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...Maxime Dénès
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-27Fixing an old bug in collecting evars with cleared context.Hugo Herbelin
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
2017-09-19test-suite: polymorphismMatthieu Sozeau
2017-09-19Allow declaring universe binders with no constraints with @{|}Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-09-19Merge PR #920: kernel: bugfix in filter_stack_domain.Maxime Dénès
2017-09-18Add test-suite script by Cyprien ManginMatthieu Sozeau
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...Maxime Dénès
2017-09-12Fixing little inaccuracy in coercions to ident or name.Hugo Herbelin
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-08-21Fixing another regression with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
2017-08-21Fixing a new regresssion with 8.4 wrt to βι-normalization of created hyps.Hugo Herbelin
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-07-31Change the option for cumulativityAmin Timany
2017-07-31Add Jason's example of fun-ext with cumulativityAmin Timany
2017-07-31Add test for NonCumulative inductivesAmin Timany
2017-07-31Issue error on monomorphic cumulative inductivesAmin Timany
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-06 16:28:48 +0000