diff options
| author | herbelin | 1999-12-15 15:24:13 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-15 15:24:13 +0000 |
| commit | d44846131cf2fab2d3c45d435b84d802b1af8d43 (patch) | |
| tree | 20de854b9ba4de7cbd01470559e956451a1d5d8e /proofs | |
| parent | 490c8fa3145e861966dd83f6dc9478b0b96de470 (diff) | |
Nouveaux types 'constructor' et 'inductive' dans Term;
les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 14 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 5 |
2 files changed, 10 insertions, 9 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 027ceab4a4..353472f019 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -281,14 +281,14 @@ let prim_refiner r sigma goal = | DOP2(Prod,c1,DLAM(_,b)) -> if k = 1 then (try - find_minductype env sigma c1 + let _ = find_minductype env sigma c1 in () with Induc -> error "cannot do a fixpoint on a non inductive type") else check_ind (k-1) b | _ -> error "not enough products" in - let _ = check_ind n cl in + check_ind n cl; if mem_sign sign f then error "name already used in the environment"; let a = mk_assumption env sigma cl in let sg = mk_goal info (push_var (f,a) env) cl in @@ -300,7 +300,7 @@ let prim_refiner r sigma goal = | DOP2(Prod,c1,DLAM(_,b)) -> if k = 1 then (try - find_minductype env sigma c1 + fst (find_minductype env sigma c1) with Induc -> error "cannot do a fixpoint on a non inductive type") else @@ -308,10 +308,10 @@ let prim_refiner r sigma goal = | _ -> error "not enough products" in let n = (match ln with (Num(_,n))::_ -> n | _ -> assert false) in - let (sp,_,_) = destMutInd (fst (check_ind n cl)) in + let (sp,_) = check_ind n cl in let rec mk_sign sign = function | (ar::lar'),(f::lf'),((Num(_,n))::ln')-> - let (sp',_,_) = destMutInd (fst (check_ind n ar)) in + let (sp',_) = check_ind n ar in if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); @@ -331,12 +331,12 @@ let prim_refiner r sigma goal = | DOP2(Prod,c1,DLAM(_,b)) -> check_is_coind b | b -> (try - let _ = find_mcoinductype env sigma b in true + let _ = find_mcoinductype env sigma b in () with Induc -> error ("All methods must construct elements " ^ "in coinductive types")) in - let _ = List.for_all check_is_coind (cl::lar) in + List.iter check_is_coind (cl::lar); let rec mk_sign sign = function | (ar::lar'),(f::lf') -> if mem_sign sign f then diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 4593e92b77..dff9fe0b2e 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -62,8 +62,9 @@ val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr val pf_nf_betaiota : goal sigma -> constr -> constr val pf_one_step_reduce : goal sigma -> constr -> constr -val pf_reduce_to_mind : goal sigma -> constr -> constr * constr * constr -val pf_reduce_to_ind : goal sigma -> constr -> section_path * constr * constr +val pf_reduce_to_mind : goal sigma -> constr -> inductive * constr * constr +val pf_reduce_to_ind : + goal sigma -> constr -> section_path * constr * constr val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (int list * section_path) list -> goal sigma -> constr -> constr |