| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10140 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10139 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
need to make NZOrdAxiomsSig a subtype of NAxiomsSig.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10132 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
the latter is bound to a var which is not a quantified one - this led
to remove a line marked "temporary compatibility" ... ; made a distinction
between quantified hypothesis as for "intros until" and binding names as
in "apply with"; in both cases, we now expect that a identifier not used
as a variable, as in "apply f_equal with f:=g" where "f" is a true binder
name in f_equal, must not be used as a variable elsewhere [see
corresponding change in Ints/Tactic.v])
- Fixing bug 1643 (bug in the algorithm used to possibly reuse a
global name in the recursive calls of a coinductive term)
- Fixing bug 1699 (bug in contracting nested patterns at printing time
when the return clause of the subpatterns is dependent)
- Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic)
- Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10130 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
message de Benjamin Pierce de sep 2007 sur coq-club) [report de la
révision 10128 de la 8.1 vers le trunk]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10127 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10125 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
-----------------------------------------------
- Les fonctions evar_define et real_clean font un travail plus fin :
- S'il y a plusieurs manières d'inverser l'instance d'une evar, on
retarde le choix au lieu de faire un choix arbitraire.
- Si l'instance contient une evar et que cette evar n'est pas inversible,
on essaie aussi d'inverser ou de restreindre (un sous-terme) de
l'evar qui était initialement à instancier.
- Incidemment, real_clean est renommé en invert_instance, un nom qui
reflète mieux la diversité du travail fait par ce fameux real_clean.
- La fonction solve_refl garde les problèmes qui contiennent encore de
l'information.
- Changements secondaires :
- Délégation de la gestion des variables modifiées et des problèmes à
reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord
au moment du define) (incidemment get_conv_pbs devient
extract_conv_pbs)
- Essai d'un mécanisme différent de restriction des evars : pour
éviter des contextes mal formés (comme do_restrict pouvait a priori
le faire), on utilise maintenant un contexte bien formé doublé d'un
filtre signalant les instances interdites. C'est a priori plus
souple (par ex : si une variable du contexte a un type dépendant
d'une evar, on peut attendre de connaître cette evar avec de
déterminer si cette variable du contexte, qui peut-être dépend via
cette evar d'une autre variable interdite, doit être finalement
interdite ou pas)
- Nettoyages divers.
- Ce que evarutil ne fait toujours pas :
- Utiliser l'inversion et/ou l'unification d'ordre supérieur (par
exemple pour résoudre "?ev[S n]=n"); en particulier, la notion
d'inversion unique ne prend pas en compte l'unification d'ordre
supérieur et peut donc faire des choix irréversibles vis à vis de
l'unif d'ordre supérieur.
- Utiliser (systématiquement -- et précautionneusement) les types
des solutions trouvées pour résoudre davantage de problèmes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10124 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
de solutions distinctes faites modulo égalité d'alias uniquement et pas
modulo toute la puissance de la convertibilité)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10123 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
the patch by S. Mimram)
* for detecting architecture, also look for /bin/uname
* restore the compatibility of kernel/byterun/coq_interp.c with
ocaml 3.07 (caml_modify vs. modify). There is still an issue
with this 3.07 and 64-bits architecture (see coqdev and a future
bug report).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10120 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Adding Qlt_shift_div_l, etc
- Adding Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).
- Adding Qle_Qabs : forall a, a <= Qabs a.
- Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs. It is
already defined elsewhere (in it's proper place).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
a few errors of parentheses around fun x -> ... constructs,
a use of tclTHEN was left over from bug tracking modifications, it
was badly parenthesized.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10117 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10116 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
evdref si evar_defs ref)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
alias de variables dans la fonction d'inversion des instance (real_clean):
- détection des cas d'inversions distinctes incompatibles
- nouvelle heuristique lorsque plusieurs inversions distinctes mais
compatibles existent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10111 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
de "projection" lors de l'instanciation d'une evar -- fonction "real_clean")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10109 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10108 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10107 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
et Set Whelp Getter pour changer le nom des serveurs (report 10105 de
la 8.1 vers le trunk)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
+ Formattage affichage arguments evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10104 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
triviales en provenance de l'algo de compilation du filtrage) lors du
calcul de la projection des variables dans real_clean
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10103 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
échouer sur les Rel liées a des Anonymous et export de l'instance
des evars vers le printeur du débogueur.
- Suppression d'un reste de code mort lié à la V7 dans pretyping.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
rationals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10101 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
rec argument, example given by Brian Aydemir.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
inequalities generation for multiple patterns.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
conjuncts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
l'unification sait maintenant résoudre des équations du genre
"?n[...;x:=?m[...;y:=t;...]] = t" lorsque x et y sont uniques vérifiant
cette propriété (la solution est alors de poser ?m:=y et ?n:=x); le
type de t est aussi pris en compte dans cette situation (ce genre de
problème permet de résoudre des cas simples d'unification avec dépendance:
cf l'exemple de foldrn dans test-suite/success/Fixpoint.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
-rectypes)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
points-fixes: on applique maintenant cette contrainte avant de
généraliser corps et types vis à vis du context (utile notamment en
présence de let-in dont on ne sait pas sinon s'ils font partie de la
contrainte de type ou du contexte de typage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- Des open en plus dans le débogueur-traceur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
pour imposer un ordre précis des répertoires (résout en partie le
problème entre Init.Wf et Program.Wf.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 85f007b7-540e-0410-9357-904b9bb8a0f7
|