diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 23:45:54 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 23:49:45 +0100 |
| commit | 486acdd7b50d4fdc0956011b7b48dc6ba96dd4a8 (patch) | |
| tree | 658279e2d0c3cf85e47c4f4d74e2c701fab18dd7 /pretyping/patternops.ml | |
| parent | af291869bb7d1184d8e655906572d75937ca829b (diff) | |
Fix interpretation of Ltac patterns episode 2.
After 5db9588098f9f, some extra evar-normalization remained (compared to trunk)
that would change the semantics e.g. of change bindings under Ltac match.
This is just circumventing a fundamental flaw in the treatment of patterns.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 8c6b39b7e..d6a7c5192 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -153,7 +153,7 @@ 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 (EConstr.to_constr sigma (Retyping.expand_projection env sigma p (EConstr.of_constr 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) -> @@ -218,7 +218,7 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in - pattern_of_constr env sigma (EConstr.to_constr 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 |