aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Add an e_type_of to avoid losing universe constraints.Gravatar Matthieu Sozeau2014-06-20
|
* Adding a raw_goals primitive for Tacinterp.Gravatar Pierre-Marie Pédrot2014-06-19
|
* - Fix bug in unification, not only named metas are turned into evars (e.g. ↵Gravatar Matthieu Sozeau2014-06-19
| | | | | | in Ssreflect). - Fix is_applied_rewrite_relation to look for propositional relations.
* HoTT coq bug #62 fixed.Gravatar Matthieu Sozeau2014-06-19
|
* Support dropping files over the coqide window. (Partial fix for bug #2765)Gravatar Guillaume Melquiond2014-06-19
| | | | | | | | 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.
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
| | | | | | 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.
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
|
* Dummy commit to test the new setup of coq-commits mailinglist (bis)Gravatar Pierre Letouzey2014-06-17
|
* Dummy commit to test the new setup of coq-commits mailinglistGravatar Pierre Letouzey2014-06-17
|
* Fix a destArity that does not exactly match isArity in presence of let-ins.Gravatar Matthieu Sozeau2014-06-17
|
* Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Gravatar Matthieu Sozeau2014-06-17
|
* Not a bug, keep for backwards compatibilityGravatar Matthieu Sozeau2014-06-17
|
* Bug closed, now in polymorphic mode, Variables A B : Type give different ↵Gravatar Matthieu Sozeau2014-06-17
| | | | levels to A and B.
* Explicit universes allow to write liftings explicitely. Implicit lifting ↵Gravatar Matthieu Sozeau2014-06-17
| | | | | | would change the theory non-trivially.
* Not considering test-suite file #89 as a bug anymore.Gravatar Matthieu Sozeau2014-06-17
|
* Continue fix on argument scopes of primitive projections.Gravatar Matthieu Sozeau2014-06-17
|
* Fix HoTT bug #84, binding scopes to projections.Gravatar Matthieu Sozeau2014-06-17
|
* HoTT coq bug #82 already fixed.Gravatar Matthieu Sozeau2014-06-17
|
* Adapt coercion code to work with projections as target classes.Gravatar Matthieu Sozeau2014-06-17
|
* Tentative optimization not to nf_evar too often in the compatibilityGravatar Pierre-Marie Pédrot2014-06-17
| | | | | | 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.
* Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).Gravatar Hugo Herbelin2014-06-17
| | | | | Thanks to David M. Cooke on coq-bugs for pointing out one part of the problem.
* Fixing #3282 (two bugs in the presence of let-in's in "fix").Gravatar Hugo Herbelin2014-06-17
|
* Complying an ocaml warning.Gravatar Hugo Herbelin2014-06-17
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
|
* Fix type inference of the record argument of a projection to catch ill-typedGravatar Matthieu Sozeau2014-06-17
| | | | applications earlier.
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
| | | | | - Fix HoTT coq bug #80, implicit arguments with primitive projections were wrongly automatically infered.
* Fix a de Bruijn bug in checking code of projections.Gravatar Matthieu Sozeau2014-06-17
|
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
| | | | | | | 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).
* Existing Class now works with universe polymorphism. Fixes HoTT bug #063Gravatar Matthieu Sozeau2014-06-17
|
* Improve hotspot in Auto.Gravatar Pierre-Marie Pédrot2014-06-17
|
* Checking that a library name is valid before compilation.Gravatar Pierre-Marie Pédrot2014-06-16
| | | | Fixes bug #3333.
* Unification in HoTT_coq_061.v was looping with previous commit (whileGravatar Hugo Herbelin2014-06-16
| | | | | | | 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.
* Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,Gravatar Hugo Herbelin2014-06-16
| | | | | 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).
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
| | | | - Remove dead code in evarconv.
* HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Gravatar Matthieu Sozeau2014-06-16
|
* Fix spacing in error message.Gravatar Guillaume Melquiond2014-06-16
|
* Preemptively remove files from native compilation.Gravatar Guillaume Melquiond2014-06-16
| | | | | | 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.
* Fix test-suite fileGravatar Matthieu Sozeau2014-06-15
|
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
| | | | | bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics.
* The semantics of Variable x y : T is to have the exact same type T for x and y,Gravatar Matthieu Sozeau2014-06-15
| | | | while Context gives different type to each variable, this test-suite file shows this.
* Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.Gravatar Matthieu Sozeau2014-06-15
|
* - Fix xml plugin treatment of inductives.Gravatar Matthieu Sozeau2014-06-15
| | | | - Move HoTT bug #30 to closed
* Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead ↵Gravatar Matthieu Sozeau2014-06-13
| | | | | | | | 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.
* HoTT/coq bug #7 is closed, and the definitions can be made to go through ↵Gravatar Matthieu Sozeau2014-06-13
| | | | | | using explicit universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
|
* Remove documentation for the unsupported options -byte and -opt.Gravatar Guillaume Melquiond2014-06-13
|
* Deprecate useless option -unsafe.Gravatar Guillaume Melquiond2014-06-13
|
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
| | | | | | | These options no longer have any impact on the way proofs are loaded. In other words, loading is always lazy, whatever the options. Keeping them just so that coqc dies when the user prints some opaque symbol does not seem worth it.
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-13
|
* Improving tclWITHHOLES which did not see undefined evars up toGravatar Hugo Herbelin2014-06-13
| | | | | restriction, after last fix commit which precisely possibly restricts evars of a term "t" in "apply t in H" without resolving them.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-18 16:12:37 +0000