diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /plugins/firstorder/formula.ml | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
Diffstat (limited to 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index b34a36492..79f185d18 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -79,13 +79,13 @@ type kind_of_formula= let kind_of_formula gl term = let normalize=special_nf gl in let cciterm=special_whd gl term in - match match_with_imp_term cciterm with - Some (a,b)-> Arrow(a,(pop b)) + match match_with_imp_term (project gl) cciterm with + Some (a,b)-> Arrow(a,(pop (EConstr.of_constr b))) |_-> - match match_with_forall_term cciterm with + match match_with_forall_term (project gl) cciterm with Some (_,a,b)-> Forall(a,b) |_-> - match match_with_nodep_ind cciterm with + match match_with_nodep_ind (project gl) cciterm with Some (i,l,n)-> let ind,u=destInd i in let (mib,mip) = Global.lookup_inductive ind in @@ -96,7 +96,7 @@ let kind_of_formula gl term = let has_realargs=(n>0) in let is_trivial= let is_constant c = - Int.equal (nb_prod c) mib.mind_nparams in + Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) @@ -108,7 +108,7 @@ let kind_of_formula gl term = else Or((ind,u),l,is_trivial) | _ -> - match match_with_sigma_type cciterm with + match match_with_sigma_type (project gl) cciterm with Some (i,l)-> Exists((destInd i),l) |_-> Atom (normalize cciterm) |