diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 74c0eb4cc7..a23c51495c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - ~allow_patvar:false c + c (* Construct a fixpoint as a Glob_term @@ -200,13 +200,13 @@ let is_rec names = | GIf(b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | GProd(na,_,t,b) | GLambda(na,_,t,b) -> - lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b | GLetIn(na,b,t,c) -> - lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c | GLetTuple(nal,_,t,b) -> lookup names t || lookup (List.fold_left - (fun acc na -> Nameops.name_fold Id.Set.remove na acc) + (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) names nal ) @@ -734,7 +734,7 @@ let rec add_args id new_args = CAst.map (function CAppExpl((None,r,None),new_args) | _ -> b end - | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") + | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) @@ -782,9 +782,9 @@ let rec add_args id new_args = CAst.map (function Miscops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) - | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") - | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") - | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") + | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") + | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.") + | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.") ) exception Stop of Constrexpr.constr_expr @@ -826,7 +826,7 @@ let rec chop_n_arrow n t = chop_n_arrow new_n t' with Stop t -> t end - | _ -> anomaly (Pp.str "Not enough products") + | _ -> anomaly (Pp.str "Not enough products.") let rec get_args b t : Constrexpr.local_binder_expr list * @@ -856,7 +856,7 @@ let make_graph (f_ref:global_reference) = | _ -> raise (UserError (None, str "Not a function reference") ) in (match Global.body_of_constant_body c_body with - | None -> error "Cannot build a graph over an axiom !" + | None -> error "Cannot build a graph over an axiom!" | Some body -> let env = Global.env () in let sigma = Evd.from_env env in @@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.out_name n),None)) + CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) |