search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.65k stars 630 forks source link

Anomaly: search error #1478

Closed coqbot closed 21 years ago

coqbot commented 21 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#261 From: monate@lix.polytechnique.fr Reported version: 8.1

coqbot commented 21 years ago

Full_Name: Benjamin Monate Version: 7.4 cvs du 05/03/03 OS: Linux dario 2.4.20v1 BZ#2 Tue Jan 7 16:58:25 CET 2003 i686 Intel(R) Pentium(R) III Mobile CPU 1133MHz GenuineIntel GNU/Linux Submission from: lri8-232.lri.fr (129.175.8.232)

Bonjour, En essayant de faire un fixpoint mal typé, j'obtiens une anomalie :

./coqtop

Welcome to Coq 7.4 (Feb 2003)

Coq < Inductive list : nat -> Set := | Nil : (list O) | Cons : (n:nat)bool->(list n)->(list (S n)).

Fixpoint rev [n:nat;l:(list n);m:nat;acc:(list m)] : (list m) := Cases l of | Nil => acc | (Cons (S n) b l) => (rev n l (S m) (Cons (S m) b acc)) end. Coq < Coq < list is defined list_rect is defined list_ind is defined list_rec is defined

Coq < Coq < Coq < Coq < Coq < Coq < Coq < Anomaly: Search error. Please report.

Coq <

Cordialement Benjamin Monate

coqbot commented 16 years ago

Fixed 1/04/03 HH