aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-20Introducing an intermediary type "constr_prod_entry_key" for grammar ↵Hugo Herbelin
productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 18:00:33 +0000