aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-20Canonically add an encoding in glob_constr of "as" operator for cases_pattern.Hugo Herbelin
2018-02-20Minor clarifying of name variables in constrintern.ml.Hugo Herbelin
- renaming lvar into ntnvars when relevant, for consistency - renaming sometimes genv into env (intern_env) so as to remain consistent with other parts of the code
2018-02-20Using name given by user to name a 'pat, if any.Hugo Herbelin
This works for contexts in Definition and co, but not yet for "fun" and co.
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
2018-02-20Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Hugo Herbelin
2018-02-20Notations: Do not consider a non-occurring variable as a binder-only variable.Hugo Herbelin
2018-02-20More precise explanation when a notation is not reversible for printing.Hugo Herbelin
2018-02-20Adding support for re-folding notation referring to isolated "forall '(x,y), t".Hugo Herbelin
Was apparently forgotten in a67bd7f9.
2018-02-20Again one more step in fixing #5762 ("where" clause).Hugo Herbelin
We enforce that variables of the notation hide the variables in the implicit-arguments map. Will be useful when there will be a special map of single binders when interpreting notations.
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Maxime Dénès
constraints.
2018-02-19Merge PR #6761: Remove unused argument in Record.declare_structureMaxime Dénès
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-19Merge PR #6753: [toplevel] Make toplevel state into a record.Maxime Dénès
2018-02-19Merge PR #6230: Better Cemitcodes API + compact relocation representationMaxime Dénès
2018-02-19Merge PR #6759: detype_case predicate is not optionalMaxime Dénès
2018-02-19Merge PR #6772: Cleanup inferCumulativityMaxime Dénès
2018-02-19Merge PR #6648: [tactics] make apply_type safeMaxime Dénès
2018-02-19Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Maxime Dénès
camlp4
2018-02-19Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Maxime Dénès
2018-02-19Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.Maxime Dénès
2018-02-19Merge PR #6571: Fix ci-all targetMaxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
longer use camlp4.
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-16Cleaner treatment of parameters in inferCumulativityGaëtan Gilbert
No using a mutable counter to skip them, instead we keep them in the environment.
2018-02-16Fix reduction flags in inferCumulativityGaëtan Gilbert
The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
2018-02-16Adding a test for the construction that was broken in Coccinelle.Pierre-Marie Pédrot
There was no test in the test-suite checking for double with-def constraints in module typing.
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
We defer the computation of the universe quantification to the upper layer, outside of the kernel.
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier.
2018-02-15[ide] Localize a IDE-specific flag.Emilio Jesus Gallego Arias
2018-02-15Merge PR #1073: new quick2vo target: like vio2vo, but smarterMaxime Dénès
2018-02-15disable tests: vio2vo is broken in WindowsRalf Jung
2018-02-15also test vio2voRalf Jung
2018-02-15test "make quick2vo"Ralf Jung
2018-02-15new quick2vo target: like vio2vo, but smarterRalf Jung
2018-02-15Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProjectMaxime Dénès
2018-02-15coq_makefile: Support "" as the prefix in _CoqProjectJoachim Breitner
This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it.
2018-02-15Merge PR #6760: CHANGES for 8.7.2.Maxime Dénès
2018-02-14CHANGES for 8.7.2.Théo Zimmermann
2018-02-14Remove unused argument in Record.declare_structureGaëtan Gilbert
This was for autoinstance.
2018-02-14Factorize the relocations in the on-disk VM representation.Pierre-Marie Pédrot
Instead of using a linear representation, we simply use a table that maps every kind of relocation to the list of positions it needs to be applied to.
2018-02-14Use a more compact representation for bytecode relocations stored on disk.Pierre-Marie Pédrot
The previous implementation used a list of pairs, which has size 9n where n is the number of relocations. We instead use two arrays for a total memory cost of 2n + 5 words. The use of arrays may turn out to be problematic on 32-bit machines, I am unsure if we will hit this limitation in practice.
2018-02-14Do not use global variables for VM bytecode compilation in Cemitcodes.Pierre-Marie Pédrot
Instead we thread a buffer.
2018-02-14Remove the unsafe bytes conversion function in Cemitcodes.Pierre-Marie Pédrot
This is actually not needed, as the only thing we do with this Bytes.t is to pass it to a C function which will use it in a read-only way.
2018-02-14Move the call to the computation of bytecode inside Cemitcodes.Pierre-Marie Pédrot
This shouldn't matter because the tcode_of_code function is pure, its only effect being allocating a string and filling it with the translated bytecode.
2018-02-14Abstract further the type of VM bytecode compilation.Pierre-Marie Pédrot
This reduces the possibility to wreak havoc while making the API nicer.
2018-02-14detype_case predicate is not optionalGaëtan Gilbert
2018-02-14Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Maxime Dénès
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-14[build] Fix VM dynamic linking prep in byte builds.Emilio Jesus Gallego Arias
We correctly set the path of `libcoqrun` in non-local builds. This bug was introduced by #6038. c.f. #6475 , #5992.
2018-02-13coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGaëtan Gilbert
(and alist-alist)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 19:12:54 +0000