aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
* Correction message d'erreur ltac et adoption du modèle de message de TacinterpGravatar herbelin2006-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout nat_path et find_referenceGravatar herbelin2006-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation du section_path pour le parsing des notations primitives,Gravatar herbelin2006-02-04
| | | | | | | | 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
* Adaptation message d'erreur au cas des stringGravatar herbelin2006-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du test du bon nombre d'argument des constructeurs (et deGravatar herbelin2006-01-30
| | | | | | | | | 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
* Nettoyage warning (dont flush et affichage seulement si mode verbose)Gravatar herbelin2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 'match x in I' (potentiellement utilisable comme cast)Gravatar herbelin2006-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7946 85f007b7-540e-0410-9357-904b9bb8a0f7
* exporting the global reference to the inductive " \/ " in coqlib andGravatar bertot2006-01-25
| | | | | | | | 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
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
| | | | | | | | 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
* Version préliminaire d'inversion de la compilation du filtrageGravatar herbelin2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomGravatar herbelin2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
* Résidus du traducteur v7 -> v8Gravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Résidus du traducteur v7 -> v8Gravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | 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
* Suppression redondance coerce_to_id dans Pcoq et constrintern et ↵Gravatar herbelin2006-01-09
| | | | | | déplacement dans Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte, enfin, du contexte des types de retour de ACases et RCasesGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de notations numérales définies au niveau utilisateur + ↵Gravatar herbelin2006-01-08
| | | | | | traitement dans alias de motifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enregistrement dans glob.dump des utilisations de notations numériques (qui ↵Gravatar herbelin2006-01-08
| | | | | | 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
* Automatisation de l'utilisation de token primitifs dans les motifs de ↵Gravatar herbelin2006-01-08
| | | | | | 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
* Ajout rawconstr_of_aconstrGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ↵Gravatar herbelin2006-01-05
| | | | | | 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
* Suppression des coercions non seulement avant l'affichage des notations mais ↵Gravatar herbelin2006-01-04
| | | | | | 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
* Redéclaration de la notation à l'import pour être cohérent avec ↵Gravatar herbelin2006-01-03
| | | | | | 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
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵Gravatar herbelin2005-12-30
| | | | | | 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
* Ajout booléens; nettoyageGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite correction nom QuantHypArgType suite suppression traducteurGravatar herbelin2005-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (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
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bugs commit précédentGravatar herbelin2005-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | 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
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de la correction du test sur le nombre de parametres d'une projectionGravatar herbelin2005-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conséquences nettoyage pretyping.mlGravatar herbelin2005-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de l'utilisation des notations récursives pour faire une ↵Gravatar herbelin2005-06-03
| | | | | | notation alternative de l'application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adoption du nom canonique global_of_constr pour éviter confusion avec type ↵Gravatar herbelin2005-05-20
| | | | | | reference git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement et export de locate_global (ex-locate_reference) de tacinterp ↵Gravatar herbelin2005-05-20
| | | | | | vers syntax_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving centralised discharge into dispatched discharge_function; required to ↵Gravatar herbelin2005-02-18
| | | | | | 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
* Standardisation of function names about global references (especially, ↵Gravatar herbelin2005-02-18
| | | | | | 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
* Bug affichage rawconstrGravatar herbelin2005-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour cible make docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
| | | | | | | "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
* HUGE COMMITGravatar sacerdot2005-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵Gravatar herbelin2005-01-03
| | | | | | printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6554 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵Gravatar herbelin2005-01-02
| | | | | | 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.39.1) at 2025-01-14 15:20:04 +0000