aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Collapse)Author
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Maxime Dénès
wish #4129)
2018-03-08Add test-suite file for cumulative constructorsMatthieu Sozeau
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
Following up on #6791, we the option "Shrink Abstract".
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵Maxime Dénès
a record.
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-03Adding a test file for evar handling in the VM.Pierre-Marie Pédrot
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
Noticed by Sigurd Schneider.
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
2018-02-20Notations: Do not consider a non-occurring variable as a binder-only variable.Hugo Herbelin
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-16Cleaner treatment of parameters in inferCumulativityGaëtan Gilbert
No using a mutable counter to skip them, instead we keep them in the environment.
2018-02-13Fixing an anomaly in the presence of "let-in" in the type of a record.Hugo Herbelin
Was raised by Jason on Gitter.
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
This ensures by construction that we never infer constraints outside the variance model.
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
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
The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else.
2018-01-03Fix core hint database issue #6521Anton Trunov
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Maxime Dénès
Extraction Language command
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 ↵Maxime Dénès
instance.
2017-11-29Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵Maxime Dénès
of levels
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
Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
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
Also nicer error when the constraints are impossible.
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
We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
2017-11-20Fixing factorization of recursive notations in the case of an atomic separator.Hugo Herbelin
This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Maxime Dénès
(clause "where" with implicit arguments)
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 14:52:11 +0000