aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml/cic2acic.ml
Commit message (Collapse)AuthorAge
* Clarification role de library_part : renommage en remove_section_partGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message d'erreur plus informatifGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8754 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
* 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
* pas besoin de List.length pour savoir si une liste est videGravatar letouzey2005-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7306 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
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
| | | | | | | | | to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | 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
* hiding the meta_map in evar_defsGravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
* The innersort is now computed as the more precise sort between theGravatar sacerdot2004-09-08
| | | | | | | | | | | | | | synthesized innersort and the expected innersort. This closes a bug that allowed to export non well-typed* terms like the following one: ((fun (X : (T1 : CProp)) => (E : (T2 : Type))) : (T1 -> T2 : CProp)) * non well-typed according to the rules that consider CProp as a primitive sort. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6082 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* - recent changes to doubleTypeInference.ml (that introduced doubleGravatar sacerdot2004-07-08
| | | | | | | | | | | | | | type inference for inferred types) undone. Previous performance restored. - bug in cic2acic (code that used to be dead fixed): the type of a sort was computed as the sort itself - CPropRetyping in cic2acic modified to handle correctly the sort Set in the two cases Predicative Set / Impredicative Set - CPropRetyping.get_type_of used in place of Retyping.get_type_of everywhere in cic2acic. This closes (again, but more efficiently) the bug about CProps erroneously recognized as Types in inferred types git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit to perform double type inference also on inner types.Gravatar sacerdot2004-07-08
| | | | | | | | | | | | | | | | | * Motivation: the inner sorts computed for the inner types were computed by Coq itself. Thus Nijmegen's CProp was exported as Type. To export CProp as CProp I have to implement a CProp-aware single type inference. To avoid the reimplementation I use double type inference. * Known problems: the double type inference algorithm is slower than the usual type inference algorithm. Moreover too many types and sorts are computed in this way. As a consequence the exportation module is now much slower (the exportation time seems to be doubled in the average case). In the future I will try to restore the original performances. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Licence changed from GPL to Lesser GPL.Gravatar sacerdot2004-06-26
| | | | | | | DTDs licence is still GPL. This should create no problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copyright notice of files in contrib/xml made uniform.Gravatar sacerdot2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoRN CProp detection improved: products of "sort" CProp are now recognizedGravatar sacerdot2004-04-07
| | | | | | | (they used to be exported as products of sort Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fake dependent products in inductive definition types are no longer replacedGravatar sacerdot2004-04-06
| | | | | | | | | | with non dependent products. The main motivation is that inductive definition parameters often occurs as non-dependent products in the product types, but the binder names are still necessary to render the definition in the usual Coq way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5646 85f007b7-540e-0410-9357-904b9bb8a0f7
* ~keep_sections was now redundant. Got rid of.Gravatar sacerdot2004-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fake dependent types in constructors of inductive types are now preserved.Gravatar sacerdot2004-03-31
| | | | | | | | | | | The idea is: 1. constructors are always declare by hand by the user ==> binders always have a meaning. 2. the binders are fundamental for record fields, even if the dependent product is really non-dependent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5621 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntax error: dandling inGravatar sacerdot2004-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5612 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2 choix incorrectsGravatar herbelin2004-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fabrication de l'uri a partir du path utilisateurGravatar herbelin2004-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix and Cofix blocks with mutually defined functions having the sameGravatar sacerdot2004-03-25
| | | | | | | | | | | | | | | | name generated XML code with ambiguous names. Example: Inductive t : Set := k : t' -> t with t' : Set := k' : t -> t'. Scheme t_csc := Induction for t Sort Prop with t'_csc := Induction for t' Sort Prop. Print XML t_csc. used to show two functions both named F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comment removed.Gravatar sacerdot2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5559 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Claudio pour v8Gravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5552 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit netoyage dans libGravatar coq2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration de la branche mowgliGravatar herbelin2002-11-05
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3213 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-25 17:58:33 +0000