aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| * | | | | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | | | | | | | | | | | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
| * | | | | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* | | | | | Adding test for #4811.Gravatar Hugo Herbelin2016-07-02
|/ / / / /
* | | | | Merge branch 'reduction-flags' into trunkGravatar Maxime Dénès2016-07-01
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction function names, itself a revision of PR#117: Isolating flags for cofix/fix reduction + adjusting names of reduction functions to what they do
| * | | | | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
| | | | | |
| * | | | | Make semantics of whd_zeta consistent with other whd_* functions.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | whd_zeta now takes an evar_map and looks in evar instances. This changes the behavior of whd_zeta e.g. on let x := ?t in x
| | * | | | Fixing use of "Declare Implicit Tactic" in refine.Gravatar Hugo Herbelin2016-07-01
| | | | | |
| * | | | | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
| * | | | Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Gravatar Hugo Herbelin2016-07-01
| | | | |
| * | | | Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Gravatar Hugo Herbelin2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | But there are still bugs with Declare Implicit Tactic, which should probably rather be reimplemented with ltac:(tac). Indeed, it does support evars in the type of the term, and solve_by_implicit_tactic should transfer universe constraints to the main goal. E.g., the following still fails, at Qed time. Definition Foo {T}{a : T} : T := a. Declare Implicit Tactic eassumption. Goal forall A (x : A), A. intros. apply Foo. Qed.
| | | * | Makefile: $(BEST) controls which coqtop is used to build .voGravatar Pierre Letouzey2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows to grant a wish by Hugo: to build coqtop.byte and prelude with it, you could do: make -j BEST=byte states
| | | * | coq_makefile : do not build bytecode versions of plugins by defaultGravatar Pierre Letouzey2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | make install does not install these *.cm(o|a) files either. You could always do manually : - make bytefiles : to build the bytecode *.cm(o|a) files - make install-byte : to install these files - make byte : to compile the whole development with the bytecode version of Coq (this builds the *.cm(o|a) files, but also the .vo via coqc -byte). Technically, the behavior of make is controlled by the OPT variable, which could be -byte or -opt. For instance, 'make byte' corresponds to a 'make OPT:=-byte' Note that coqdep is used with the new option "-dyndep var" : when seeing a Declare ML Module "foo", "coqdep -dyndep var" does not decide whether to depend on foo.cma or foo.cmxs, but rather use some Makefile variables such as foo$(DYNLIB), whose content is later set according to $(OPT)
| | | * | Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see next commit about coq_makedile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* | | | Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Gravatar Hugo Herbelin2016-06-29
| | | | | | | | | | | | | | | | See 4865.v for details.
* | | | Exporting section_segment_of_reference.Gravatar Hugo Herbelin2016-06-29
| | | |
* | | | Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
| | | |
* | | | Merge branch 'programcases' into trunkGravatar Matthieu Sozeau2016-06-29
|\ \ \ \
| * | | | Fixes in documentation.Gravatar Matthieu Sozeau2016-06-29
| | | | |
| * | | | Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
* | | | Merge branch 'bug4527' into trunkGravatar Matthieu Sozeau2016-06-29
|\ \ \ \
| * | | | Univ: Use loc even if there are more unbound levelsGravatar Matthieu Sozeau2016-06-29
| | | | |
| * | | | CHANGES: document fix for #4726 too.Gravatar Matthieu Sozeau2016-06-29
| | | | |
| * | | | CHANGES: document fix for 4527 and compatibility.Gravatar Matthieu Sozeau2016-06-29
| | | | |
| * | | | universes.ml: Minor code cleanupGravatar Matthieu Sozeau2016-06-29
| | | | |
| * | | | Univs: Fix bug #4726Gravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | When using Record and an explicit sort constraint, the universe was wrongly made flexible and minimized.
| * | | | Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | For better error messages. The API change is backwards compatible, using a new optional argument.
| * | | | Univs: earlier errors for strict univ decls #4527Gravatar Matthieu Sozeau2016-06-29
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | When declaring the universes of a lemma explicitely, throw an error if after minimization the type of a lemma still refers to unbound universes. This is a fix and an incompatibility, but scripts will be backwards compatible themselves. Fix another minor bug in treating universe binders for (Co)Fixpoint.
* | | | Merge branch 'warnings' into trunkGravatar Maxime Dénès2016-06-29
|\ \ \ \ | | | | | | | | | | | | | | | Was PR#213: New warnings machinery
| * | | | Fix issues in test-suite revealed by warnings.Gravatar Maxime Dénès2016-06-29
| | | | |
| * | | | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
| * | | | Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
| | | * | fix coqide double module linking (error on OCaml 4.03)Gravatar Gabriel Scherer2016-06-28
| | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Linking the same module twice in OCaml can have problematic unintended consequences and lead to hard-to-understand bugs, see http://caml.inria.fr/mantis/view.php?id=4231 http://caml.inria.fr/mantis/view.php?id=5461 OCaml has long warned when double-linking happens Warning 31: files FOO and BAR both define a module named Baz In 4.03 this error was turned into a warning by default. Coqide does double-linking by passing both xml_{lexer,parser,printer}.cmo and lib/clib.cma that already contains these compilation units to bin/coqide.byte. To fix compilation of Coqide under 4.03, the present patch removes the .cmo from the command-line arguments. P.S.: I checked that this patch applies cleanly to the current trunk (b161ad97fdc01ac8816341a089365657cebc6d2b). It should also be possible to add it as a patch on top of the 8.5 archives (for example those distributed through OPAM) to make them compile under 4.03.
* | | | Revert "A new infrastructure for warnings."Gravatar Maxime Dénès2016-06-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0. I forgot that Jenkins gave me a spurious success when trying to build this PR. There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue has been fixed by Matej. Sorry for the noise.
* | | | Typeclasses: use once in by clause for typeclass eautoGravatar Matthieu Sozeau2016-06-28
| | | | | | | | | | | | | | | | | | | | Otherwise we may backtrack on the resolution in a by which seems strange.
* | | | Merge branch 'warnings' into trunkGravatar Maxime Dénès2016-06-28
|\ \ \ \ | | | | | | | | | | | | | | | Was PR#213: New warnings machinery
| * | | | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-28
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* | | | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \ \ \ | |/ / / |/| | | | | | | Was PR#207: Add -no-print-dependent-evars
| | * | Merge branch 'forhott' into v8.5Gravatar Matthieu Sozeau2016-06-28
| | |\ \
* | | \ \ Finalizing the only printing feature.Gravatar Pierre-Marie Pédrot2016-06-28
|\ \ \ \ \
| * | | | | Documenting the "only printing" notation flag.Gravatar Pierre-Marie Pédrot2016-06-28
| | | | | |
| * | | | | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
| | | | | |
| * | | | | Properly handle the only printing flag in Reserved Notations.Gravatar Pierre-Marie Pédrot2016-06-28
| | | | | |
| * | | | | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
|/ / / / /
| | | * | Univs/CHANGES: #4097 and annotations on notationsGravatar Matthieu Sozeau2016-06-27
| | | | |
| | | * | Refine fix for bug #4097, avoid proj expansionGravatar Matthieu Sozeau2016-06-27
| | | | |
| | | * | Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | | | | | They can apply to the head reference under a notation.
| | | * | Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
| | |/ / | | | | | | | | | | | | | | | | | | | | internalization. Patch by PMP, test-suite fix by MS.
* | | | Merge branch 'shrinkobl' into trunkGravatar Matthieu Sozeau2016-06-27
|\ \ \ \
| * | | | Update CHANGES and COMPATIBILITYGravatar Matthieu Sozeau2016-06-27
| | | | |
| * | | | Program: refine shrinking of obligationsGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Ensure correspondence between the term and type to shrink, so that Lets are preserved when they are used relevantly in either of them. This avoids e.g. "simpl" in the shrinked hypotheses to reduce shrinking, while maintaining unsimplified types in the type of the shrinked obligations (for compatibility). Simplify Lambda, Prod case of shrinking, By invariant (we start with a term and its type), the abstraction's types correspond.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 21:10:59 +0000