aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2004-12-09Achèvement correction bug do_restrict_hys: ne pas inverser les argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6454 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6437 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Correction d'un bug historique de do_restrict_hyps + code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Bugs dans la déclaration du type du terme filtré si non définiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6433 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-08Bug nom exceptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6432 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Relâchement obligation d'une contrainte de type sur les Hole en position ↵herbelin
terminale, pour plus grande généralité de understand_gen_tcc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06C'est trop compliqué de mettre à jour les types du metamap en passant sous ↵herbelin
les lieurs, plus simple de garder le type avec un cast (cf bug #889) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6415 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Commentaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6405 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Propagation du nom des hyps du prédicat de filtrage pour le message ↵herbelin
d'erreur elim_arity et réparation dans build_initial_predicate du bug mentionné dans success/Case8.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6394 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29UserError in reduce_to_*_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6382 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26Correction bug #879herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6357 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26MAJ PCoFixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6352 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6330 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-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17Vérification de la typability de 'pattern'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6226 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27?(mod_delta=true) parameter added to each unification function.sacerdot
mod_delta = true if the unification is done modulus delta conversion (of closed terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6142 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27collapse apps of patterns to avoid failuresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6139 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-25Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ↵herbelin
sub_match qui est renommé par ailleurs en match_subterm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6133 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-23error if binder was already definedbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6122 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 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-12inclusion de meta_map dans evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10simplification de clenvbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08unification encore...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08petit bug avec les effets de bordsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6078 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient ↵herbelin
incorrects: 0 au lieu de 1 et lv dans le mauvait sens) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6075 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06mimick: unify types before making assignationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6067 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06bad env in mimick codebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6065 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03deplacement de clenv vers pretypingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Expansion du prédicat du 'match' vis à vis de la dépendance en le terme ↵herbelin
filtré (utilisation de Anonymous pour signaler une dépendance formelle, en relation avec le nommage dans Inductiveops.type_case_branches); uniformisation/nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6032 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Prise en compte expansion du prédicat du 'match' vis à vis de la ↵herbelin
dépendance en le terme filtré (cf Indrec) + déplacement routines pour Cases à la V7 dans Pretyping) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6031 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵herbelin
inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 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-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-07-13bug #794: conv made in wrong envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5897 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #790: better error_not_cleanbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5896 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Eta-expansion du predicat dans build_indrec (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5887 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Eta-expansion du predicat pas seulement pour make_case mais aussi pour ↵herbelin
build_indrec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5884 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ↵herbelin
(c'est au moment de la construction dans Indrec qu'il faut eta-expanser -cf bug #784) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5883 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30updated printing of evar context (may loop ?)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5853 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Double bug d'affichage des cases dépendants (bug #784)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5837 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 04:19:07 +0000