diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /plugins/funind/glob_term_to_relation.ml | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 4b6caea70d..02964d7ba5 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -478,7 +478,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid | GApp(_,_) -> @@ -588,6 +588,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") | GProd _ -> user_err Pp.(str "Cannot apply a type") + | GInt _ -> user_err Pp.(str "Cannot apply an integer") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -1221,7 +1222,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) let rec compute_cst_params relnames params gt = DAst.with_val (function - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params | GApp(f,args) -> begin match DAst.get f with | GVar relname' when Id.Set.mem relname' relnames -> |