diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:56:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 18:56:18 +0200 |
| commit | a52d06ea16cff00faa7d2f63ad5c1ca0b58e64b4 (patch) | |
| tree | 40440d7daed82bd24180b36ef224f245ddca42f5 /interp | |
| parent | 30a908becf31d91592a1f7934cfa3df2d67d1834 (diff) | |
| parent | a321074cdd2f9375662c7c9f17be5c045328bd82 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 4 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0e5602078..8520bd5d8 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -33,10 +33,10 @@ open Context.Rel.Declaration (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments - - it remplaces notations by their value (scopes stuff are here) + - it replaces notations by their value (scopes stuff are here) - it recognizes global vars from local ones - - it prepares pattern maching problems (a pattern becomes a tree where nodes - are constructor/variable pairs and leafs are variables) + - it prepares pattern matching problems (a pattern becomes a tree + where nodes are constructor/variable pairs and leafs are variables) All that at once, fasten your seatbelt! *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 1e14eeb81..b020f8945 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -45,10 +45,10 @@ let dump_string s = if dump () && !glob_output != Feedback then Pervasives.output_string !glob_file s -let start_dump_glob vfile = +let start_dump_glob ~vfile ~vofile = match !glob_output with | MultFiles -> - open_glob_file (Filename.chop_extension vfile ^ ".glob"); + open_glob_file (Filename.chop_extension vofile ^ ".glob"); output_string !glob_file "DIGEST "; output_string !glob_file (Digest.to_hex (Digest.file vfile)); output_char !glob_file '\n' diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index a7c799114..e84a64052 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -9,7 +9,7 @@ val open_glob_file : string -> unit val close_glob_file : unit -> unit -val start_dump_glob : string -> unit +val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6b29b6d3d..2f3ebcc9b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -125,7 +125,7 @@ let rec cases_pattern_fold_map loc g e = function e', PatCstr (loc,cstr,patl',na') let subst_binder_type_vars l = function - | Evar_kinds.BinderType (Name id) as e -> + | Evar_kinds.BinderType (Name id) -> let id = try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in |