diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-06 00:24:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-06 00:24:57 +0200 |
| commit | cc0f9d254c394db742473299336fb20b82ae4aa1 (patch) | |
| tree | cbc89906c862624d4285f367d1fa9f0f61f16f05 /pretyping/patternops.ml | |
| parent | b377bd30f23f430882902f534eaf31b1314ecd07 (diff) | |
| parent | 88fdd28815747520bdc555a2d1b8600e114ab341 (diff) | |
Merge PR#716: Don't double up on periods in anomalies
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 71dbc39f3..db2e5da95 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -112,14 +112,14 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") + | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") 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 | Var id -> VarRef id - | _ -> anomaly (Pp.str "Not a rigid reference") + | _ -> anomaly (Pp.str "Not a rigid reference.") let pattern_of_constr env sigma t = let rec pattern_of_constr env t = |