diff options
Diffstat (limited to 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 62a8605a3d..b34a364920 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,9 +16,11 @@ open Util open Declarations open Globnames +module RelDecl = Context.Rel.Declaration + let qflag=ref true -let red_flags=ref Closure.betaiotazeta +let red_flags=ref CClosure.betaiotazeta let (=?) f g i1 i2 j1 j2= let c=f i1 i2 in @@ -58,12 +60,12 @@ let ind_hyps nevar ind largs gls= Array.map myhyps types let special_nf gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let special_whd gl= - let infos=Closure.create_clos_infos !red_flags (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) type kind_of_formula= Arrow of constr*constr @@ -139,8 +141,8 @@ let build_atoms gl metagen side cciterm = negative:= unsigned :: !negative end; let v = ind_hyps 0 i l gl in - let g i _ (_,_,t) = - build_rec env polarity (lift i t) in + let g i _ decl = + build_rec env polarity (lift i (RelDecl.get_type decl)) in let f l = List.fold_left_i g (1-(List.length l)) () l in if polarity && (* we have a constant constructor *) @@ -150,8 +152,8 @@ let build_atoms gl metagen side cciterm = | Exists(i,l)-> let var=mkMeta (metagen true) in let v =(ind_hyps 1 i l gl).(0) in - let g i _ (_,_,t) = - build_rec (var::env) polarity (lift i t) in + let g i _ decl = + build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -224,7 +226,7 @@ let build_formula side nam typ gl metagen= | And(_,_,_) -> Rand | Or(_,_,_) -> Ror | Exists (i,l) -> - let (_,_,d)=List.last (ind_hyps 0 i l gl).(0) in + let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in |