diff options
| author | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
| commit | 835be3a05e28eb6e26f703a034f22b2c6c61acaa (patch) | |
| tree | 00ecf04840ba027c3c71f8503d9811c8a5dc1d2e /pretyping/patternops.ml | |
| parent | 0980dbb1740c8d48d8ff0c516929f27f8cea854d (diff) | |
| parent | 2e6a89238dc7197057d0da80a16f4b4b1e41bfd8 (diff) | |
Merge PR#379: Introducing evar-insensitive constrs
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 79765a4938..318f94be24 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -116,7 +116,7 @@ let rec head_pattern_bound t = | PLambda _ -> raise BoundPattern | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") -let head_of_constr_reference c = match kind_of_term c with +let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> ConstRef sp | Construct (sp,_) -> ConstructRef sp | Ind (sp,_) -> IndRef sp @@ -155,18 +155,14 @@ let pattern_of_constr env sigma t = | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> - pattern_of_constr env (Retyping.expand_projection env sigma p c []) + pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> - let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in - let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> - let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in - let () = ignore (pattern_of_constr env ty) in PMeta None) | Case (ci,p,a,br) -> let cip = @@ -211,6 +207,8 @@ let error_instantiate_pattern id l = ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") let instantiate_pattern env sigma lvar c = + let open EConstr in + let open Vars in let rec aux vars = function | PVar id as x -> (try @@ -222,7 +220,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - pattern_of_constr env sigma c + pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in |