diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 34 | ||||
| -rw-r--r-- | interp/declare.ml | 9 | ||||
| -rw-r--r-- | interp/impargs.ml | 9 |
3 files changed, 26 insertions, 26 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 838ef40545..70ce6cef19 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -716,20 +716,20 @@ let rec flatten_application c = match DAst.get c with (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = - try - let (sc,n) = uninterp_prim_token r in - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> - match availability_of_prim_token n sc scopes with - | None -> None - | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)) - with No_match -> - None - -let extern_optimal_prim_token scopes r r' = - let c = extern_possible_prim_token scopes r in - let c' = if r==r' then None else extern_possible_prim_token scopes r' in + let (sc,n) = uninterp_prim_token r in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> + match availability_of_prim_token n sc scopes with + | None -> raise No_match + | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + +let extern_possible extern r = + try Some (extern r) with No_match -> None + +let extern_optimal extern r r' = + let c = extern_possible extern r in + let c' = if r==r' then None else extern_possible extern r' in match c,c' with | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match @@ -769,12 +769,14 @@ let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal_prim_token scopes r r' + extern_optimal (extern_possible_prim_token scopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations r'') + extern_optimal + (fun r -> extern_notation scopes vars r (uninterp_notations r)) + r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with diff --git a/interp/declare.ml b/interp/declare.ml index a9bfe8cabb..1e972d3e35 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -358,10 +358,6 @@ let inInductive : mutual_inductive_entry -> obj = let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = let id = Label.to_id label in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - Recordops.declare_primitive_projection p; - (* ^ needs to happen before declaring the constant, otherwise - Heads gets confused. *) let univs = match univs with | Monomorphic_ind_entry _ -> (** Global constraints already defined through the inductive *) @@ -378,7 +374,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter Vars.subst_instance_constr u term, Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in - ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent)) + let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + Recordops.declare_primitive_projection p cst + let declare_projections univs mind = let env = Global.env () in diff --git a/interp/impargs.ml b/interp/impargs.ml index d8582d856e..d024a9e808 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -19,7 +19,6 @@ open Decl_kinds open Lib open Libobject open EConstr -open Termops open Reductionops open Constrexpr open Namegen @@ -200,16 +199,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc acc.(i) <- update pos rig acc.(i) | App (f,_) when rig && is_flexible_reference env sigma bound depth f -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Proj (p,c) when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Case _ when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Evar _ -> () | _ -> - iter_constr_with_full_binders sigma push_lift (frec rig) ed c + iter_with_full_binders sigma push_lift (frec rig) ed c in let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc |