Debug implementation of dependent induction/dependent destruction and document it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10490 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 59 insertions, 8 deletions

diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index f8e225bd4..cce04b4e2 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1,7 +1,7 @@
 @String{jfp   = "Journal of Functional Programming"}
 @String{lncs  = "Lecture Notes in Computer Science"}
 @String{lnai  = "Lecture Notes in Artificial Intelligence"}
-@String{SV    = "{Sprin\-ger-Verlag}"}
+@String{SV    = "{Sprin­ger-Verlag}"}
 
 @InProceedings{Aud91,
   author      = {Ph. Audebaud},
@@ -426,7 +426,7 @@ s},
   editor      = {G. Huet and G. Plotkin},
   pages       = {59--79},
   publisher   = {Cambridge University Press},
-  title       = {Inductive sets and families in {Martin-L{\"o}f's}
+  title       = {Inductive sets and families in {Martin-Löf's}
  Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, 
   volume      = {14},
   year        = {1991}
@@ -446,7 +446,7 @@ s},
   author      = {J.-C. Filli\^atre},
   month       = sep,
   school      = {DEA d'Informatique, ENS Lyon},
-  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}},
+  title       = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. Étude et impl\'ementation dans le syst\`eme {\Coq}},
   year        = {1994}
 }
 
@@ -460,7 +460,7 @@ s},
 }
 
 @Article{Filliatre03jfp,
-  author      = {J.-C. Filli{\^a}tre},
+  author      = {J.-C. Filliâtre},
   title       = {Verification of Non-Functional Programs 
                  using Interpretations in Type Theory},
   journal     = jfp,
@@ -478,7 +478,7 @@ s},
 @PhDThesis{Filliatre99,
   author      = {J.-C. Filli\^atre},
   title       = {Preuve de programmes imp\'eratifs en th\'eorie des types},
-  type        = {Th{\`e}se de Doctorat},
+  type        = {Thèse de Doctorat},
   school      = {Universit\'e Paris-Sud},
   year        = 1999,
   month       = {July},
@@ -597,7 +597,7 @@ s},
   author      = {D. Hirschkoff},
   month       = sep,
   school      = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris},
-  title       = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
+  title       = {Écriture d'une tactique arithm\'etique pour le syst\`eme {\Coq}},
   year        = {1994}
 }
 
@@ -870,7 +870,7 @@ Intersection Types and Subtyping},
 }
 
 @MastersThesis{Mun94,
-  author      = {C. Mu{\~n}oz},
+  author      = {C. Muñoz},
   month       = sep,
   school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
   title       = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
@@ -980,7 +980,7 @@ the Calculus of Inductive Constructions}},
   institution = {INRIA},
   month       = nov,
   number      = {1795},
-  title       = {{D{\'e}veloppement de l'Algorithme d'Unification dans le Calcul des Constructions}},
+  title       = {{Développement de l'Algorithme d'Unification dans le Calcul des Constructions}},
   year        = {1992}
 }
 
@@ -1153,6 +1153,57 @@ Languages},
   year        = {1987}
 }
 
+@inproceedings{DBLP:conf/types/CornesT95,
+  author    = {Cristina Cornes and
+               Delphine Terrasse},
+  title     = {Automating Inversion of Inductive Predicates in Coq},
+  booktitle = {TYPES},
+  year      = {1995},
+  pages     = {85-104},
+  crossref  = {DBLP:conf/types/1995},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@proceedings{DBLP:conf/types/1995,
+  editor    = {Stefano Berardi and
+               Mario Coppo},
+  title     = {Types for Proofs and Programs, International Workshop TYPES'95,
+               Torino, Italy, June 5-8, 1995, Selected Papers},
+  booktitle = {TYPES},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {1158},
+  year      = {1996},
+  isbn      = {3-540-61780-9},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@inproceedings{DBLP:conf/types/McBride00,
+  author    = {Conor McBride},
+  title     = {Elimination with a Motive},
+  booktitle = {TYPES},
+  year      = {2000},
+  pages     = {197-216},
+  ee        = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
+  crossref  = {DBLP:conf/types/2000},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
+@proceedings{DBLP:conf/types/2000,
+  editor    = {Paul Callaghan and
+               Zhaohui Luo and
+               James McKinna and
+               Robert Pollack},
+  title     = {Types for Proofs and Programs, International Workshop, TYPES
+               2000, Durham, UK, December 8-12, 2000, Selected Papers},
+  booktitle = {TYPES},
+  publisher = {Springer},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {2277},
+  year      = {2002},
+  isbn      = {3-540-43287-6},
+  bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+
 @Comment{cross-references, must be at end}
 
 @Book{Bastad92,