diff options
Diffstat (limited to 'COPYRIGHT')
| -rw-r--r-- | COPYRIGHT | 8 |
1 files changed, 1 insertions, 7 deletions
@@ -20,12 +20,6 @@ parsing/search.ml) Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier) Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml) -Coq includes a tactic Jp based on JProver, a theorem prover for -first-order intuitionistic logic. Jprover was originally implemented -by Stephan Schmitt and then integrated into MetaPRL by Aleksey -Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL -and then integrated it into Coq. - The file CREDITS contains a list of past contributors The credits section in Reference Manual introduction details contributions. @@ -38,4 +32,4 @@ The Coq development Team (march 2004) Pierre Letouzey (Université Paris Sud) Claude Marché (Université Paris Sud-INRIA) Christine Paulin (Université Paris Sud) - Clément Renard (INRIA)
\ No newline at end of file + Clément Renard (INRIA) |