aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixing compilation with old CAMLPX versions.Gravatar Pierre-Marie Pédrot2015-12-05
|
* Factorizing unsafe code by relying on the new Dyn module.Gravatar Pierre-Marie Pédrot2015-12-05
|
* Leveraging GADTs to provide a better Dyn API.Gravatar Pierre-Marie Pédrot2015-12-05
|
* Making output of target source-doc a bit less verbose.Gravatar Hugo Herbelin2015-12-05
|
* Fixing compilation of mli documentation.Gravatar Hugo Herbelin2015-12-05
| | | | | Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed.
* Fix to previous commit (ClassicalFacts.v).Gravatar Hugo Herbelin2015-12-05
|
* Adding proofs on the relation between excluded-middle and minimization.Gravatar Hugo Herbelin2015-12-05
| | | | | | | In particular, a proof of the equivalence of excluded-middle and an unrestricted principle of minimization. Credits to Arnaud Spiwack for the ideas and formalizations of the proofs.
* Removing redundant versions of generalize.Gravatar Hugo Herbelin2015-12-05
|
* Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml.
* Slight simplification of the code of primitive projection (in relationGravatar Hugo Herbelin2015-12-05
| | | | | to c71aa6b and 6ababf) so as to rely on generic functions rather than re-doing the de Bruijn indices cooking locally.
* Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file.
* Simplifying an instantiation function using subst_of_rel_context_instance.Gravatar Hugo Herbelin2015-12-05
|
* About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev.
* Experimenting documentation of the Vars.subst functions.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | | | | | | | Related questions: - What balance to find between precision and conciseness? - What convention to follow for typesetting the different components of the documentation is unclear? New tentative type substl to emphasize that substitutions (for substl) are represented the other way round compared to instances for application (applist), though there are represented the same way (i.e. most recent/dependent component on top) as instances of evars (mkEvar). Also removing unused subst*_named_decl functions (at least substnl_named_decl is somehow non-sense).
* Contracting one extra beta-redex on the fly when typing branches of "match".Gravatar Hugo Herbelin2015-12-05
|
* A few renaming and simplification in inductive.ml.Gravatar Hugo Herbelin2015-12-05
|
* Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
|
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
| | | | | next to each other, waiting for possible integration into a more uniform API.
* An example in centralizing similar functions to a common place so thatGravatar Hugo Herbelin2015-12-05
| | | | | cleaning the interfaces is eventually easier. Here, adding find_mrectype_vect to simplify vnorm.ml.
* Using x in output test-suite Cases.v (cosmetic).Gravatar Hugo Herbelin2015-12-05
|
* Ensuring that documentation of mli code works in the presence of utf-8Gravatar Hugo Herbelin2015-12-05
| | | | characters.
* Getting rid of some quoted tactics in Tauto.Gravatar Pierre-Marie Pédrot2015-12-05
|
* Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
| | | | | | Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point.
* Getting rid of the dynamic node of the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Removing the last use of valueIn in Tauto.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Getting rid of dynamic hacks in Setoid_newring.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Removing the globTacticIn primitive.Gravatar Pierre-Marie Pédrot2015-12-03
| | | | | It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee.
* Fixing Tauto compilation for older versions of OCaml.Gravatar Pierre-Marie Pédrot2015-12-03
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\
* | Removing the last use of tacticIn in setoid_ring.Gravatar Pierre-Marie Pédrot2015-12-03
| |
* | Removing the use of tacticIn in Tauto.Gravatar Pierre-Marie Pédrot2015-12-03
| |
| * Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
| |
| * Slight simplification of code for pat/constr.Gravatar Hugo Herbelin2015-12-02
| |
| * Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
| | | | | | | | | | | | pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though.
| * Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
| |
| * Update history of revisions.Gravatar Hugo Herbelin2015-12-02
| |
| * Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
| |
| * Univs/Program: update the universe context with global universeGravatar Matthieu Sozeau2015-12-02
| | | | | | | | | | constraints at the time of Next Obligation/Solve Obligations so that interleaving definitions and obligation solving commands works properly.
| * Fix bug #4444: Next Obligation performed after a Section opening wasGravatar Matthieu Sozeau2015-12-02
| | | | | | | | | | | | | | using the wrong context. This is very bad style but currently unavoidable, at least we don't throw an anomaly anymore.
| * Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
| | | | | | | | projections (off by default).
| * Fix a bug in externalisation which prevented printing of projectionsGravatar Matthieu Sozeau2015-12-02
| | | | | | | | using dot notation.
* | Removing dead code in Obligations.Gravatar Pierre-Marie Pédrot2015-12-02
| |
* | New algorithm for universe cycle detections.Gravatar Jacques-Henri Jourdan2015-12-01
| |
* | Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
| | | | | | | | | | | | longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l).
| * vio: fix argument parsing (progress on #4442)Gravatar Enrico Tassi2015-12-01
| |
* | Simplify coqdep lexer by removing global references.Gravatar Guillaume Melquiond2015-11-30
| |
| * Test for bug #4149.Gravatar Pierre-Marie Pédrot2015-11-30
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Test-suite files for closed bugsGravatar Matthieu Sozeau2015-11-28
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 00:38:37 +0000