aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-10-24Ajout de la tactique "apply in".herbelin
Au passage, déplacement des tactiques cut and co plus en amont + commentaires. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9266 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Hack peu élégant pour permettre de parser des listes avec séparateurs dans herbelin
TACTIC EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9265 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Interprétation du terme comme type dans 'change' si pas de 'with' (pour ↵herbelin
bénéficier des coercions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9264 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23fixed same_file (#1141)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9263 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23fixed non-bug #1213barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9262 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23bug #1194: normalisation evars a la sortie de focusbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9261 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23Fixed "Show intros" which did not look at hypothesis.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9260 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23Add a flush after backtracking x y z and before printing subgoals.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9259 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-23Add a flush for a warning.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9258 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-21Le calcul de la classe dans class_args_of ne suivait pas celui de class_ofherbelin
(avec comme conséquence des échecs en cas de beta-redex - cf coercions.v). Allègements triviaux dans coercion.ml en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9257 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-21Pas d'@ dans les identificateurs (pour F4 and co)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9256 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-21Correction d'un vieux bug de coercion avec éta-expansion (utilisationherbelin
de subst1 au lieu de subst_term). Indentation plus compacte au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9255 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9254 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Correction du bug #1255 (réécriture setoid sous un produit)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9253 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Correction de la localisation des erreurs en interactif (numéro deherbelin
ligne relatif à la ligne au lieu de absolu par rapport à la session) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9252 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-20Starting to add a function schemes merging command (not finished, notcourtieu
activated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9251 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-19Correction sym -> commherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9250 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-19coqide: affichage des sous-buts et hypothèses et métas comme types deherbelin
telle sorte que les coercions vers sortclass ne soient pas affichées (comme dans coqtop) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17field_simplify_eq profite de la factorisation de Laurentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9248 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Clarification des contraintes sur le contexte de paramètres desherbelin
inductifs dans le test de sous-typage (exigence du même nombre d'arguments uniformes attendus mais pas d'exigence spéciale sur les définitions locales du contexte à partir du moment où les types et constructeurs sont convertibles quand généralisés par rapport au contexte de paramètres) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9247 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Noms "canoniques" pour certaines des propriétés de xor.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9246 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16affichage des ... dans les scriptsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16typo doc + bug legacy fieldbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9243 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16changes the use of lists and notations, to avoid that the notationsbertot
from BinList hide the 'List' type as soon as one requires a ring tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9242 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13Simplification ocamldebug (coq-debug-programs.out obsolète)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9241 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13Ajout des options Coqide suggérées par Damien Doligez (wish #1053)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9240 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13Adaptation des tests suite à la modification de Rewrite .. in (r9201)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9239 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13Correction test-suite suite à r9186notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9238 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13Ajout du théorème mult_minus_distr_lnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9237 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-13 r9778@tannat: jforest | 2006-10-13 11:36:37 +0200jforest
Changement de nom des lemme de correction/completude des Functions vis a vis de leur graphes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9236 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-12Protection raise en début de séquence (en attendant que le code caché ↵herbelin
trouve sa place) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9235 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-12Fix name clash on leftthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9234 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-11Ajout de pages de man pour les exécutables coqnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9233 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-11Ajout d'une option -annotate au configure+ changement du comportement par ↵notin
défaut de make git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9232 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-10Fix 0 obligations bugmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9231 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-10Remove duplicate conditions in Field + Monomial substitution function for PExprthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9230 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-10make sure BinList is not made visible to files that use the tactic Ringbertot
because BinList contains an abbreviation to cons that makes printing of lists strange. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9229 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Exemple avec liaison des variables de filtrage du matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9228 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Amélioration de l'automatisation des coupures quand deux idents se suiventherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9227 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Notations:herbelin
- prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Ajout combinateurs option_fold_left et name_fold_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06suite commit 9222 : rétablissement des tests autre que complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9224 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Remplacement des nf_evar (source de complexité polynomiale) par de laherbelin
réduction paresseuse. Accessoirement, suppression d'un test evar_defined inutile car sur résultat de whd_betadeltaiota qui contient la réduction evar de tête dans coercion.ml; code mort du commit précédent dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Ajout d'un répertoire de test de la complexitéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9222 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Déplacement de on_judgment_type de Typeops vers Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Suppression d'une source de complexité polynomiale dans le pretypageherbelin
(remplacement de la normalisation complète des evars dans les termes par une normalisation par nécessité - dans les types, c'est en général des expressions plus petites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9220 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9219 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Annulation de l'essai de changement de sémantique du %scope (révision 9208).herbelin
Retour à une sémantique où les %scope s'appliquent à la sous-expression complète (trop de pbs: constantes polymorphes sans arguments scope, variables locales de type fonctionnel, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9218 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ↵notin
d'un constr c, on vérifie que c est clos dans l'environnement de m (#1183) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9217 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-10 23:44:29 +0000