| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16543 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16498 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
fixpoint definition
+ Help the use of #trace on evar_conv_appr_x
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
destruct, rewrite, etc. is not well-typed.
Also added support for a more informative message when the elimination
predicate is not well-formed while using the smart "second-order"
unification algorithm. However the "abstract_list_all" algorithm seems
to remain more informative though, so we still use this algorithm for
reporting about ill-typed predicates.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It uses a term in front of a stack instead of a term in front of a list of applied
terms. From outside of eq_appr_x nothing should have changed.
Nasty evar instantiation bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
occurrences to abstract can be given. This allows to force "destruct"
to necessarily abstract over all occurrences of its main argument
(only the sub-arguments that occur in the inductive type of the main
argument have their occurrences constrained by typing). This
incidentally avoids "rewrite" succeeding in rewriting only a part of
the occurrences it has to rewrite. This repairs the failure of
RecursiveDefinition which failed after pattern unification fix from
r14642).
Full support for selecting occurrence of main argument still to be
done though.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14648 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
second-order matching) which was not working correctly in the general
case.
Also made that second-order matching for tactics (abstract_list_all)
uses this algorithm, along the lines of a proposal first experimented
by Dan Grayson (see unification.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
problems with dependencies. Generalized it to matching over dependent
tuples as explored by Dan Grayson. Currently used only in Evarconv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
informative exception if some constraints do not unify.
All calls except one used to raise a less informative exception when the
constraints weren't solved.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
major changes in [w_unify] and the conversion functions used by it to
handle the sort constraints correctly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[set_eq_sort_variable] for cases where two universes should be equal,
fix [evars_reset_evd] to keep sort constraints and use [whd_sort_var]
directly in [whd_evar].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12149 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort
constraints are thrown away at the end of unification for the moment,
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unification algorithm. Uses the same code to recognize projections
(check_conv_record) and the same unification steps on the solution as
evar_conv. This required to fold the sigma through unify_* along with
the meta and evar substitutions as this can grow during unification.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12128 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
en dernière étape de la procédure d'unification
- Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution
de l'unification premier ordre flexible/rigide
- Déplacement check_evars dans Evarutil
Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
(cf exemples d'application dans test-suite/success/evars.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- reduction du noyau (variables existentielles, fonctions auxiliaires
pour inventer des noms, etc. deplacees hors de kernel/)
- changement de noms de constructeurs des constr (suppression de "Is" et
"Mut")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@735 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- unsafe_env -> env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@161 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@102 85f007b7-540e-0410-9357-904b9bb8a0f7
|
