diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-01 20:53:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:21:51 +0100 |
| commit | 8f6aab1f4d6d60842422abc5217daac806eb0897 (patch) | |
| tree | c36f2f963064f51fe1652714f4d91677d555727b /plugins/funind/glob_term_to_relation.ml | |
| parent | 5143129baac805d3a49ac3ee9f3344c7a447634f (diff) | |
Reductionops API using EConstr.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index de2e5ea4e..92de4d873 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -352,7 +352,7 @@ let add_pat_variables pat typ env : Environ.env = | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env (Evd.from_env env) typ + try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in @@ -409,7 +409,7 @@ let rec pattern_to_term_and_type env typ = function constr in let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env (Evd.from_env env) typ + try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in @@ -629,7 +629,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = - try Inductiveops.find_inductive env (Evd.from_env env) b_typ + try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ) with Not_found -> user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -661,7 +661,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = - try Inductiveops.find_inductive env (Evd.from_env env) b_typ + try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ) with Not_found -> user_err (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ |