aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-06-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7123 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7122 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07pas de filtrages partielsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7121 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la ↵barras
notion de variable de sortes (mais pas encore utilise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7118 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06essai de typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7115 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7114 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05eradication de Evarutil.w_Definebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7113 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-05assouplissement de real_clean: ne tient pas compte des occcurences flexibles ↵barras
des variables git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7112 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7110 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-04Ajout explicite du niveau 200 de pattern auquel on fait référence au ↵herbelin
niveau 0; nécessaire pour option -nois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7109 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7105 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03Prise en compte de l'utilisation des notations récursives pour faire une ↵herbelin
notation alternative de l'application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7104 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03suppression de code commentecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7103 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03whelp + correction bug affichage de coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7100 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7098 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7096 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-31coqwc: Admittedfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7095 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7093 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7091 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-28majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7089 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-28unification: evar_define checks the free variables are bound in the evar contextbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7088 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-27majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7086 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7084 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26No parentheses around f in 'f \subst{...}'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7083 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Utilisation du module Buffer; encodage plus rigoureux des symboles en uriherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7082 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Correction of a bug in functional scheme. It raised with mutualcoq
functions with imbricated recursive calls. Two bugs in one actually, one in the building of the set of recursive functions, and one with De Bruijn indices when looking for recursve calls. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7080 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Patch to avoid Whelp bug removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7079 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26Add a guard for V7 mode, CVS compiles cleanly again :)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7078 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
and coqide to control a remote browser. It uses the standard syntax where "%s" is the placeholder for the URL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7077 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7075 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25Forgot to remove a cmo.coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7074 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-25Added subtac contrib.coq
Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7071 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7070 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24Added clenv_environments_evars that behaves as clen_environments butsacerdot
generating evars in place of metas. Notice that thanks to this changement unification can be more effective (expecially after reduction) since evars have non-empty contexts whereas metas have not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7069 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24New commit to allow definitions of morphisms on relations whose carrier issacerdot
a Prod. Example: m : feq ==> feq where m has type (A -> B) -> (C -> D) and few is a relation over (fun X Y: Type. X -> Y). The problem is to avoid the interpretation (A -> B) -> C -> D that tries to use feq over D and feq over C considering (A -> B) as a quantification. This closes a wish of Bas Spitters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7068 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24WARNING: unification changed (to fix a bug).sacerdot
1. When matching ?i[sigma] against t' in some cases ?i was instantiated with t' ignoring the explicit substitution sigma (i.e. always doing mimick); however, when t' occurs in sigma ?i can be instatiated with a Var/Rel (i.e. doing projection). The new behaviour is not equivalent to the old one (even up to bugs) since the new behaviour may accept not well typed instantiations and fail only later whereas the old (but buggy) behaviour failed immediately. 2. Second bug fixed: it was the case that instantiating and evar doing projection did not check whether the body of the evar contained metavariables (that breaks a Coq invariant). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7067 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-24dp: ajout du prouveur Zenoncoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7066 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7064 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-23Consequence of allowing the numerical argument of auto to be an ident for ltacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7062 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-23Bug fix for a bug reported by Roland: the function that detects the constantssacerdot
to be expanded during functor application was written supposing that the module had already been checked against its signature. However, this is actually a false hypothesis. The bug fix consists in replacing an "assert false" with the error message that would be obtained type checking the module against its module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7061 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7059 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7057 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7055 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7054 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-20Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵herbelin
reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:11:46 +0000