aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Ajout nat_path et find_referenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7985 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-04Utilisation du section_path pour le parsing des notations primitives,herbelin
dans la mesure où le nom d'un module est différent selon qu'on est en cours de compilation (MPself) ou requis (MPfile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7984 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-31Adaptation message d'erreur au cas des stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7967 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Déplacement du test du bon nombre d'argument des constructeurs (et deherbelin
l'inductif si clause "in I ...") dans Constrintern, pour assurer notamment que les constructeurs et inductifs dans pattern (obtenu de rawconstr) ont les bonnes arités git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7957 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Nettoyage warning (dont flush et affichage seulement si mode verbose)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7954 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29Bug 'match x in I' (potentiellement utilisable comme cast)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7946 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-25exporting the global reference to the inductive " \/ " in coqlib andbertot
eq_rawconstr in topconstr to prepare the introduction of the new version of functionnal induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7928 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre d'application des Hints de auto) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Version préliminaire d'inversion de la compilation du filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7842 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Résidus du traducteur v7 -> v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-09Suppression redondance coerce_to_id dans Pcoq et constrintern et ↵herbelin
déplacement dans Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Prise en compte, enfin, du contexte des types de retour de ACases et RCasesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7823 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Prise en compte de notations numérales définies au niveau utilisateur + ↵herbelin
traitement dans alias de motifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7821 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Enregistrement dans glob.dump des utilisations de notations numériques (qui ↵herbelin
peuvent maintenant être définies au niveau utilisateur) + divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7820 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de ↵herbelin
filtrage + prise en compte de notations numérales définies au niveau utilisateur+ légère restructuration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7819 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-08Ajout rawconstr_of_aconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-05Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ↵herbelin
suppression des coercions permet aussi d'afficher un nombre, on choisit l'affichage qui n'introduit pas de délimiteurs si possible (exemple: avec 'Zpos 2', si Zpos est une coercion, on peut effacer la coercion et afficher 2 dans le type positive, ou bien garder la coercion afficher 'Zpos 2' comme 2 dans Z; dans certains cas - cf 4CT - il n'y a pas d'afficheur qui gère la coercion et il faut la retirer avant d'appliquer l'afficheur de nombre le plus interne) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7796 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Suppression des coercions non seulement avant l'affichage des notations mais ↵herbelin
aussi avant l'affichage des notations primitives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7788 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-03Redéclaration de la notation à l'import pour être cohérent avec ↵herbelin
l'activation à l'import des notations qui ne sont pas des définitions syntaxiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7779 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵herbelin
de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-30Ajout booléens; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Petite correction nom QuantHypArgType suite suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-23Simplifification de vernac_expr li l'abandon du traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Correction bugs commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7695 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-21Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7596 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-19Correction de la correction du test sur le nombre de parametres d'une projectionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7590 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Conséquences nettoyage pretyping.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7362 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-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
2005-05-20Déplacement et export de locate_global (ex-locate_reference) de tacinterp ↵herbelin
vers syntax_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7051 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵herbelin
aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about global references (especially, ↵herbelin
renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-07Bug affichage rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6696 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-06Nettoyage et documentation de Libraryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Pour cible make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6620 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03HUGE COMMITsacerdot
1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6554 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 18:49:36 +0000