aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
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
2004-12-25Passage d'une bibliothèque de grands entiers naturels vers une ↵herbelin
bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une ↵herbelin
bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-22Mecanisme d'affichage des types (notamment les conclusions des buts) ↵herbelin
typiquement pour eviter les coercions en tete git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6490 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification ↵herbelin
n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵herbelin
tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6315 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Suppression capture des variables par lieurs non liés dans Notation; ↵herbelin
simplification bound_binders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6314 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Suppression capture des variables par lieurs non liés dans Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6313 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Interpretation et affichage corrects des notations LetTuple, affichage des ↵herbelin
notations If git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6025 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus ↵herbelin
au moment de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-06Apply implicit types to local binders tooherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6017 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Suppression de Rawterm.loc, branchement sur Util.locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5911 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27Typo (bug #797)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5832 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Amélioration affichage coercions vers Funclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5799 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-08Chgt role 2eme argument AList et implantation affichage motifs recursifs de ↵herbelin
notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-06Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5640 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Heuristique pour traduire if-then-else quand le re-typage echoueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5616 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵herbelin
sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27Gestion maintenant purement fonctionnelle des implicites des point-fixes; ↵herbelin
ajout de la prise en compte dynamique des arguments scope pour les inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5586 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27Export compute_arguments_scope pour utilisation local a la construction des ↵herbelin
inductifs et points fixes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5585 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-19Bug protection array_fold_left2herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5536 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Motifs recursifs de notations: prise en compte de l'associativite et des ↵herbelin
notations de pattern de filtrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5516 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Mise en place de motifs récursifs dans Notation; quelques simplifications ↵herbelin
au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fix (2e)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5478 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5477 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de choix de noms courts avec Suresnes/BDDbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5476 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 00:40:32 +0000