diff options
| author | herbelin | 2002-04-12 15:08:51 +0000 |
|---|---|---|
| committer | herbelin | 2002-04-12 15:08:51 +0000 |
| commit | c6217e50bba82c50a8f8ec18adf4dcc5612c8607 (patch) | |
| tree | a6ec30bd7dd289035a8e630a5e33e8d270911db8 | |
| parent | ec0ae1070f15a3bc8a6f6699500b146ecd69dec3 (diff) | |
q: Commande introuvable.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2640 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/logic.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 299021926d..eb0b94671a 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -448,23 +448,23 @@ let prim_refiner r sigma goal = if b then [sg1;sg2] else [sg2;sg1] | FixRule (f,n,rest) -> - let rec check_ind k cl = + let rec check_ind env k cl = match kind_of_term (strip_outer_cast cl) with - | Prod (_,c1,b) -> + | Prod (na,c1,b) -> if k = 1 then try fst (find_inductive env sigma c1) with Not_found -> error "cannot do a fixpoint on a non inductive type" else - check_ind (k-1) b + check_ind (push_rel (na,None,c1) env) (k-1) b | _ -> error "not enough products" in - let (sp,_) = check_ind n cl in + let (sp,_) = check_ind env n cl in let all = (f,n,cl)::rest in let rec mk_sign sign = function | (f,n,ar)::oth -> - let (sp',_) = check_ind n ar in + let (sp',_) = check_ind env n ar in if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); @@ -477,10 +477,10 @@ let prim_refiner r sigma goal = mk_sign sign all | Cofix (f,others) -> - let rec check_is_coind cl = + let rec check_is_coind env cl = let b = whd_betadeltaiota env sigma cl in match kind_of_term b with - | Prod (_,c1,b) -> check_is_coind b + | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b | _ -> try let _ = find_coinductive env sigma b in () @@ -489,7 +489,7 @@ let prim_refiner r sigma goal = "in coinductive types") in let all = (f,cl)::others in - List.iter (fun (_,c) -> check_is_coind c) all; + List.iter (fun (_,c) -> check_is_coind env c) all; let rec mk_sign sign = function | (f,ar)::oth -> (try |