diff options
| author | Matej Kosik | 2016-02-17 11:16:27 +0100 |
|---|---|---|
| committer | Matej Kosik | 2016-02-17 11:16:27 +0100 |
| commit | 93c03652fea5914307b0a6b72b7fec6f9aaec305 (patch) | |
| tree | fe9e5e983452d5489550e9322d42067e4b213e19 /plugins/firstorder/formula.ml | |
| parent | 06fa0334047a9400d0b5a144601fca35746a53b8 (diff) | |
| parent | 1dddd062f35736285eb2940382df2b53224578a7 (diff) | |
CLEANUP: Context.{Rel,Named}.Declaration.t
Diffstat (limited to 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index ae2d059fa2..2ed436c6bf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -15,6 +15,7 @@ open Tacmach open Util open Declarations open Globnames +open Context.Rel.Declaration let qflag=ref true @@ -139,8 +140,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 (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 +151,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 (get_type decl)) in List.fold_left_i g (2-(List.length l)) () v | Forall(_,b)-> let var=mkMeta (metagen true) in @@ -224,7 +225,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 = get_type (List.last (ind_hyps 0 i l gl).(0)) in Rexists(m,d,trivial) | Forall (_,a) -> Rforall | Arrow (a,b) -> Rarrow in |