| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
Fixes compilation of Coq with OCaml 4.03 beta 1.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
| |\| | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\| |
| | |
| | |
| | |
| | | |
Conflicts:
lib/cSig.mli
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
|
| | | |
| | |
| | |
| | | |
There is no location to print anyway, so it will never be useful.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
|
| | | | |
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | | |
proofs.
|
| |\| | |
|
| |\ \ \ |
|
| | | | | |
|
| | |/ / |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).
Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
I was trying to be a bit too clever with not substituting the universe
instance everywhere: the constructor type/inductive arity has to be
instantiated before instantiate_params runs, which became true only
for constructor types since my last commit.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
|
| | | |
| | |
| | |
| | |
| | | |
Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Reviewed by M. Sozeau
This commit fixes template polymorphism and makes it more precise,
applying to non-linear uses of the same universe in parameters of
template-polymorphic inductives. See bug report and
https://github.com/coq/coq/pull/69 for full details.
I also removed some deadcode in checker/inductive.ml.
I do not know if it is also necessary to fix checker/indtypes.ml.
|
| | | |
| | |
| | |
| | | |
Wrong handling of mind_params_ctxt...
|
| | | |
| | |
| | |
| | |
| | | |
Adapt to new [projection] abstract type comprising a constant and
a boolean.
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
This allows fatal_error to be used for printing anomalies at loading time.
|
| | |/
|/| |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Marshalled libraries are only loaded when needed and dropped thereafter.
This might be costly for Require inside modules, but such a practice is
discouraged anyway.
|
| | |
| |
| |
| |
| | |
The first part only contains the summary of the library, while the second
one contains the effective content of it.
|
| | |
| |
| |
| | |
This allows fatal_error to be used for printing anomalies at loading time.
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| |\| |
|
| | | |
|
Pierre-Marie Pédrot
Maxime Dénès
Matej Kosik
Guillaume Melquiond
Matthieu Sozeau
mlasson
Hugo Herbelin
Matthieu Sozeau
Thomas Sibut-Pinote
Arnaud Spiwack
Pierre Boutillier
Pierre Letouzey