aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-06-20Fixed some HoTT bugs, provide a proper error message when giving an ill-formedMatthieu Sozeau
universe instance.
2014-06-20Bug 27 closed now that universe contexts can be refined during the proof,Matthieu Sozeau
here instantiating a flexible level with Set.
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
for helping fixing this). Now the issue is handled solely through refreshing of the terms assigned to evars during unification. If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention a template universe and in turn, ?X won't. Same goes when typechecking (nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh universes for the lists carriers. This also handles user-defined functions on template polymorphic inductives, which was fragile before. Pretyping and Evd are now uncluttered from template-specific code.
2014-06-20Add an e_type_of to avoid losing universe constraints.Matthieu Sozeau
2014-06-19Adding a raw_goals primitive for Tacinterp.Pierre-Marie Pédrot
2014-06-19- Fix bug in unification, not only named metas are turned into evars (e.g. ↵Matthieu Sozeau
in Ssreflect). - Fix is_applied_rewrite_relation to look for propositional relations.
2014-06-19HoTT coq bug #62 fixed.Matthieu Sozeau
2014-06-19Support dropping files over the coqide window. (Partial fix for bug #2765)Guillaume Melquiond
The fix is only partial, because dropping files only works over the menu bar, the icon bar, the status bar, and so on. Editable boxes, such as the script widget, catch dnd events, hence preventing this code from working for these drop targets. Some (labl)gtk expert should be able to sort it out.
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup.
2014-06-18Code factorization in LMap.Pierre-Marie Pédrot
2014-06-17Dummy commit to test the new setup of coq-commits mailinglist (bis)Pierre Letouzey
2014-06-17Dummy commit to test the new setup of coq-commits mailinglistPierre Letouzey
2014-06-17Fix a destArity that does not exactly match isArity in presence of let-ins.Matthieu Sozeau
2014-06-17Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Matthieu Sozeau
2014-06-17Not a bug, keep for backwards compatibilityMatthieu Sozeau
2014-06-17Bug closed, now in polymorphic mode, Variables A B : Type give different ↵Matthieu Sozeau
levels to A and B.
2014-06-17Explicit universes allow to write liftings explicitely. Implicit lifting ↵Matthieu Sozeau
would change the theory non-trivially.
2014-06-17Not considering test-suite file #89 as a bug anymore.Matthieu Sozeau
2014-06-17Continue fix on argument scopes of primitive projections.Matthieu Sozeau
2014-06-17Fix HoTT bug #84, binding scopes to projections.Matthieu Sozeau
2014-06-17HoTT coq bug #82 already fixed.Matthieu Sozeau
2014-06-17Adapt coercion code to work with projections as target classes.Matthieu Sozeau
2014-06-17Tentative optimization not to nf_evar too often in the compatibilityPierre-Marie Pédrot
layer. To this intent, we add a cache evar_map in goals that is the latest known one where the goal is nf-evarized. If the current one and the cache coincide, we leave the goal as-is.
2014-06-17Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).Hugo Herbelin
Thanks to David M. Cooke on coq-bugs for pointing out one part of the problem.
2014-06-17Fixing #3282 (two bugs in the presence of let-in's in "fix").Hugo Herbelin
2014-06-17Complying an ocaml warning.Hugo Herbelin
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-06-17Fix type inference of the record argument of a projection to catch ill-typedMatthieu Sozeau
applications earlier.
2014-06-17- Fix the de Bruijn problem in check_projection for good :)Matthieu Sozeau
- Fix HoTT coq bug #80, implicit arguments with primitive projections were wrongly automatically infered.
2014-06-17Fix a de Bruijn bug in checking code of projections.Matthieu Sozeau
2014-06-17Safer entry point of primitive projections in the kernel, now it does recognizeMatthieu Sozeau
a projection constant only of the form λ params (r : I params), match r with BuildR args => args_i end, without any other user input and relies on it being typable (no more primitive projections escaping this).
2014-06-17Existing Class now works with universe polymorphism. Fixes HoTT bug #063Matthieu Sozeau
2014-06-17Improve hotspot in Auto.Pierre-Marie Pédrot
2014-06-16Checking that a library name is valid before compilation.Pierre-Marie Pédrot
Fixes bug #3333.
2014-06-16Unification in HoTT_coq_061.v was looping with previous commit (whileHugo Herbelin
it was failing with Not_found before previous commit). This "fixes" the loop by expanding local defs in "imitate" rather than keeping them explicit. The example is otherwise too large for me to be able to understand where does the loop come from.
2014-06-16Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,Hugo Herbelin
fix the type of the term which has to be in the signature of the evar to declare); some problems remain though (see next commit).
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
- Remove dead code in evarconv.
2014-06-16HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Matthieu Sozeau
2014-06-16Fix spacing in error message.Guillaume Melquiond
2014-06-16Preemptively remove files from native compilation.Guillaume Melquiond
Ocaml does not remove the .cmi file if compilation fails, thus causing subsequent native compilations to fail due to mismatching interfaces. For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
2014-06-15Fix test-suite fileMatthieu Sozeau
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics.
2014-06-15The semantics of Variable x y : T is to have the exact same type T for x and y,Matthieu Sozeau
while Context gives different type to each variable, this test-suite file shows this.
2014-06-15Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.Matthieu Sozeau
2014-06-15- Fix xml plugin treatment of inductives.Matthieu Sozeau
- Move HoTT bug #30 to closed
2014-06-13Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead ↵Matthieu Sozeau
of an anomaly in case a universe inconsistency occurs when applying a coercion. The statement of the test-suite file cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat to Set.
2014-06-13HoTT/coq bug #7 is closed, and the definitions can be made to go through ↵Matthieu Sozeau
using explicit universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2014-06-13Deprecate useless option -unsafe.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:02:46 +0000