aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-07-14ajout des unsafeCoerce + 2 bugs haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5904 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5901 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #780: compilation of several units in the same coqtop processbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5900 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-13bugs #667 and #783 (mimick_evar and loc_table on large files)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5894 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5891 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-12MAJ techniqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5890 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5889 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-07-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5880 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5879 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5878 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08* <style>...</style> tag no longer generated for theory filessacerdot
(the HELM/MoWGLI stylesheets do not longer require it) * helm:helm_link added to each <a/> element whose href is an URI * the required <body/> element was not generated for theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5877 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08- recent changes to doubleTypeInference.ml (that introduced doublesacerdot
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
2004-07-08Commit to perform double type inference also on inner types.sacerdot
* 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
2004-07-08added commands to idecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5870 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5869 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-07bypass w_Define when w_refine-ingcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5868 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5867 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5866 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-05Constants just after a "Let id : t. ... Qed" local variable declaration weresacerdot
exported as a copy of the variable id. Fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5865 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-04majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5863 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5862 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-02syntax compatibility fixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5861 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5860 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5859 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5858 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-30instantiate entry: constr -> lconstrcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5856 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5855 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5854 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-29moved instantiate binding to extratacticscorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29License de contrib/interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5849 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-29efficacite du lexeurfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5847 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5846 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5845 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28contrib/interface *$*$@!corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5844 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28more evar stuffcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Ajout de la coercion id dans context vers evaluable constant (bug #777)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5841 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Correction bug #776herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5839 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
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau ↵letouzey
mind_record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5836 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5835 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5834 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-27Correction affichage v8 des records avec let (bug #798)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5830 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 08:36:39 +0000