diff options
Diffstat (limited to 'plugins/firstorder/formula.ml')
| -rw-r--r-- | plugins/firstorder/formula.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index db1a46a03..c55040df0 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -8,7 +8,7 @@ open Hipattern open Names -open Term +open Constr open EConstr open Vars open Termops @@ -39,7 +39,7 @@ exception Is_atom of constr let meta_succ m = m+1 let rec nb_prod_after n c= - match kind_of_term c with + match Constr.kind c with | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 1+(nb_prod_after 0 b) | _ -> 0 |