diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-16 13:02:55 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:22 +0200 |
| commit | ad3aab9415b98a247a6cbce05752632c3c42391c (patch) | |
| tree | 1fba7e25aa16dbb7e42db283f8210b31a0b8931d /plugins/funind/glob_term_to_relation.ml | |
| parent | 6d9e008ffd81bbe927e3442fb0c37269ed25b21f (diff) | |
[location] Move Glob_term.cases_pattern to located.
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4b942c989..85d465a4b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -345,12 +345,12 @@ let raw_push_named (na,raw_value,raw_typ) env = let add_pat_variables pat typ env : Environ.env = - let rec add_pat_variables env pat typ : Environ.env = + let rec add_pat_variables env (loc, pat) typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with - | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env - | PatCstr(_,c,patl,na) -> + | 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) (EConstr.of_constr typ) with Not_found -> assert false @@ -398,11 +398,11 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = function - | PatVar(loc,Anonymous) -> assert false - | PatVar(loc,Name id) -> +let rec pattern_to_term_and_type env typ = Loc.with_unloc (function + | PatVar Anonymous -> assert false + | PatVar (Name id) -> mkGVar id - | PatCstr(loc,constr,patternl,_) -> + | PatCstr(constr,patternl,_) -> let cst_narg = Inductiveops.constructor_nallargs_env (Global.env ()) @@ -430,6 +430,7 @@ let rec pattern_to_term_and_type env typ = function mkGApp(mkGRef(ConstructRef constr), implicit_args@patl_as_term ) + ) (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the |