aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Make installation of native files more robust.Gravatar Maxime Dénès2015-01-15
|
* coq_makefile installs native filesGravatar Pierre Boutillier2015-01-15
|
* Always build (even when -coqide no) and install idetoploopGravatar Pierre Boutillier2015-01-15
| | | | So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed)
* Hugo put me in credits, but I was already there :)Gravatar Maxime Dénès2015-01-15
|
* Tentatively updating credits while remaining brief.Gravatar Hugo Herbelin2015-01-15
|
* Makefile: install ide/*langGravatar Enrico Tassi2015-01-14
|
* coq_makefile: chmod 755 on toplopp cmxsGravatar Enrico Tassi2015-01-14
|
* CoqIDE: a Make file to build coqidetop toploopGravatar Enrico Tassi2015-01-14
|
* Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: document tryif/then/else.Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: document multimatch.Gravatar Arnaud Spiwack2015-01-14
|
* Reference manual: try and improve documentation for Ltac's match.Gravatar Arnaud Spiwack2015-01-14
| | | | In particular document the "once" behaviour.
* Reference manual: try and improve the documentation of lazymatch.Gravatar Arnaud Spiwack2015-01-14
| | | | In particular try to avoid the use of the word "backtracking" which refers to too many things.
* Reference manual: document gfail.Gravatar Arnaud Spiwack2015-01-14
|
* CHANGES: my recent updates to Ltac.Gravatar Arnaud Spiwack2015-01-14
| | | | | - gfail - multimatch - tryif/then/else
* Bump version and magic numbers in configure.Gravatar Maxime Dénès2015-01-13
|
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
| | | | This is a follow-up on Pierre's 5d80a385.
* Refresh some copyright headers.Gravatar Maxime Dénès2015-01-13
|
* Native compiler: if debug flag not present, remove .native files.Gravatar Maxime Dénès2015-01-13
|
* More documentation of the Local Definitions and Axioms.Gravatar Pierre-Marie Pédrot2015-01-13
|
* More in CHANGES about local definitionsGravatar Pierre-Marie Pédrot2015-01-13
|
* TCs: Properly handle Hint Extern with conclusions of the form _ -> _Gravatar Matthieu Sozeau2015-01-13
| | | | | in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
* Fix test-suite file, we were testing that no anomaly was raisedGravatar Matthieu Sozeau2015-01-13
| | | | and this is the case now.
* Update hash of cic.mli in checker/values.ml,Gravatar Matthieu Sozeau2015-01-13
| | | | letting make validate progress.
* Fix bug when discharging universe constraints coming from variablesGravatar Matthieu Sozeau2015-01-13
| | | | | | into monomorphic constants, which was still using the de Bruijn encoding Bug revealed by discharging of hidden internal monomorphic definition in otherwise polymorphic developments. Makes coqchk work on Hurkens again.
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
| | | | | | constr for primitive records (not used anywhere else than printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add some minor fixes in detyping and pretty printing related to universes.
* typo in coqide compilation rules after -thread requirementGravatar Pierre Boutillier2015-01-12
|
* Derive -> derive occurencesGravatar Pierre Boutillier2015-01-12
|
* Coq_makefile erases native compiler filesGravatar Pierre Boutillier2015-01-12
|
* fixup to vi -> vio renamingGravatar Enrico Tassi2015-01-12
|
* Whodidwhat-8.5: a global passGravatar Arnaud Spiwack2015-01-12
| | | Updating my own work and others when I could think of them.
* whodidwhat-8.5: typo.Gravatar Arnaud Spiwack2015-01-12
|
* Add -no-native-compiler flag to list dumped by --help.Gravatar Maxime Dénès2015-01-12
|
* Add myself to credits.Gravatar Maxime Dénès2015-01-12
|
* Update credits.Gravatar Guillaume Melquiond2015-01-12
|
* Fix files in test-suite having to do with Require inside modules.Gravatar Maxime Dénès2015-01-12
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Update test for #3363 now that Require is forbidden inside modules.Gravatar Maxime Dénès2015-01-12
|
* Fix a few typos.Gravatar Maxime Dénès2015-01-12
|
* Fixing name of evars in output test Notation.v.Gravatar Hugo Herbelin2015-01-12
|
* Not "Setting ?n=?p order to ?p:=?n to see if it solves someGravatar Hugo Herbelin2015-01-12
| | | | | | | incompatibilities wrt 8.4.", as it creates other problems (in Ergo and Compcert). This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.
* Fixing typo in previous commit.Gravatar Hugo Herbelin2015-01-12
|
* Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep.Gravatar Hugo Herbelin2015-01-11
|
* Avoiding a redundant information in unification error message.Gravatar Hugo Herbelin2015-01-11
|
* some credits for STMGravatar Enrico Tassi2015-01-11
|
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
|
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | After this commit, module_type_body is a particular case of module_type. For a [module_type_body], the implementation field [mod_expr] is supposed to be always [Abstract]. This is verified by coqchk, even if this isn't so crucial, since [mod_expr] is never read in the case of a module type. Concretely, this amounts to the following rewrite on field names for module_type_body: - typ_expr --> mod_type - typ_expr_alg --> mod_type_alg - typ_* --> mod_* and adding two new fields to mtb: - mod_expr (always containing Abstract) - mod_retroknowledge (always containing []) This refactoring should be completely transparent for the user. Pros: code sharing, for instance subst_modtype = subst_module. Cons: a runtime invariant (mod_expr = Abstract) which isn't enforced by typing. I tried a polymorphic typing of mod_expr, to share field names while not having mtb = mb, but the OCaml typechecker isn't clever enough with polymorphic mutual fixpoints, and reject code sharing (e.g. between subst_modtype and subst_module). In the future (with ocaml>=4), some GADT could maybe help here, but for now the current solution seems good enough.
* Extraction: discard unnecessary code inside modules without signaturesGravatar Pierre Letouzey2015-01-11
| | | | | | | In the case of an inner module without explicit signature, (and not used later in a functor application), we now extract only the needed items (used later or asked by the user), instead of blindly extracting all fields as earlier.
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
| | | | | | Since type variables are local to the definition, we simply rename them in case of unicode chars. We also get rid of any ' to avoid Ocaml illegal 'a' type var (clash with char litteral).
* Extraction : some more support functions for a future "Extraction Compute"Gravatar Pierre Letouzey2015-01-11
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 00:09:25 +0000