| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
| |
reason, Ltac interpretation does not allow tactics of the following
shape : let x := bla in TacGeneric tac. Hence we force genargs to be
tactics and build the resulting hole tactic from scratch.
|
|
|
|
|
|
| |
The original idea was to send not the kernel name, but the file/line
to that CoqIDE could make the text an hyperlink to the file, exactly
as coqdoc generated HTML.
|
|
|
|
| |
when internalizing a term.
|
|
|
|
| |
internalization time.
|
|
|
|
|
|
| |
used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.
|
|
|
|
|
|
| |
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
|
|
|
|
| |
parsing is plugged.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
To reduce the amount of syntactic noise, we now provide
a few inner modules Int.List, Id.List, String.List, Sorts.List
which contain some monomorphic (or semi-monomorphic) functions
such as mem, assoc, ...
NB: for Int.List.mem and co we reuse List.memq and so on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16736 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
of tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Clarification of the existence of three algorithms for solving
unconstrained evars:
- the type-class mechanism
- the heuristics for solving pending conversion problems and multi-candidates
- Declare Implicit Tactic (when called from tactics)
Main function for solving unconstrained evars (when not using
understand): Pretyping.solve_remaining_evars
- Clarification of the existence of three corresponding kinds of
errors when reporting about unsolved evars:
Main function for checking resolution of evars independently of the
understand functions: Pretyping.check_evars_are_solved
- Introduction of inference flags in pretyping for governing which
combination of the algorithms to use when calling some understand
function; there is also a flag of expanding or not evars and for
requiring or not the resolution of all evars
- Less hackish way of managing Pretyping.type_constraint: all three
different possibilities are now represented by three different
constructors
- Main semantical changes done:
- solving unconstrained evars and reporting is not any longer mixed:
one first tries to find unconstrained evars by any way possible;
one eventually reports on the existence of unsolved evars using
check_evars_are_solved
- checking unsolved evars is now done by looking at the evar map,
not by looking at the evars occurring in the terms to pretype; the
only observed consequence so far is in Cases.v because of subterms
(surprisingly) disappering after compilation of pattern-matching
- the API changed, see dev/doc/changes.txt
Still to do:
- Find more uniform naming schemes:
- for distinguishing when sigma is passed as a reference or as a value
(are used: suffix _evars, prefix e_)
- for distinguishing when evars are allowed to remain uninstantiated or not
(are used: suffix _evars, again, suffix _tcc, infix _open_)
- be more consistent on the use of names evd/sigma/evars or evdref/evars
- By the way, shouldn't "understand" be better renamed into "infer" or
"preinfer", or "pretype". Grammatically, "understanding a term" looks
strange.
- Investigate whether the inference flags in tacinterp.ml are really
what we want (e.g. do we really want that heuristic remains
activated when typeclasses are explicitly deactivated, idem in
Tacinterp.interp_open_constr where flags are strange).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
it into the standard logger instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16488 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A new feedback message for globalization infos can be sent by
Coq to Coqide. Coqide stores the information in the proof of
concept module wg_Tooltip, that also sets things up so that
these infos are displayed as a tooltip when the mouse is over
the text they are attached to. These infos are available only
on locked text, and on the text just processed in the case of an
error (on this piece of text, they vanish as the error tag vanishes
as soon as the user edits the text).
wg_Tooltip stocks these infos as lazy string. This is not needed
in the proof of concept, but is necessary to scale up: Coq may not
generate the full piece of info when the message is sent (because of
high computational cost or big size) and just send an id; later on,
when/if the user asks for the piece of info, the gui requests the
info explicitly using the id.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
mechanism with the SearchAbout one. Searches may be slower, but this
is unlikely to be noticed. In addition, according to Hugo, the
Libtype summary was imposing a noticeable time penalty without
any real advantage.
Now Search and SearchPattern are the same. The documentation was not
really clear about the difference between both, except that Search
was restricted to closed terms. This is an artificial restriction by
now.
Fixing #2815 btw.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16320 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
NB: this "try...with" plus the test at the next line
(if !interning_grammar || env.unb then ...)
were actually catching too many errors (for instance
error_not_enough_arguments).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16278 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
predicate in "match x return ... with" when x is a goal variable.
Commit 4926 forbade it but too strongly. AFAICS, only notation
variables have to be avoided.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
some cleaning of the interface and moving of code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
IT happens that there are some other uses of casts, e.g. in nat_int de
MathClasses which uses a notation 0 for some class constructor zero,
and a cast (0:nat) to force this notation 0 to represent the instance
O in nat of the class of types having a zero (eventually, 0,
i.e. "zero nat O" and "O" are convertible but the information of being
a class instance is lost).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15999 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
type in "cast" to activate the temporary interpretation scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
variable is used both as term and as binder, resulting in
ununderstandable error message about scopes).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|