fix: correct spelling of 'instantiate'

The spelling 'instanciate' is only acknowledged in the Wiktionary, while
all other dictionaries prefer the spelling with a 't'.

ex.: https://dictionary.cambridge.org/dictionary/english/instantiate

Author: loutr

src/ecCoreSubst.ml

@@ -14,7 +14,7 @@ type mod_extra = {
   mex_glob  : memory -> form;
 }
 
-type sc_instanciate = {
+type sc_instantiate = {
   sc_memtype : memtype;
   sc_mempred : mem_pr Mid.t;
   sc_expr    : expr Mid.t;

src/ecCoreSubst.mli

@@ -8,7 +8,7 @@ open EcCoreModules
 open EcCoreFol
 
 (* -------------------------------------------------------------------- *)
-type sc_instanciate = {
+type sc_instantiate = {
   sc_memtype : memtype;
   sc_mempred : mem_pr Mid.t;
   sc_expr    : expr Mid.t;

src/ecDecl.ml

@@ -68,7 +68,7 @@ let abs_tydecl ?(tc = Sp.empty) ?(params = `Int 0) lc =
   { tyd_params = params; tyd_type = Abstract tc; tyd_loca = lc; }
 
 (* -------------------------------------------------------------------- *)
-let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =
+let ty_instantiate (params : ty_params) (args : ty list) (ty : ty) =
   let subst = CS.Tvar.init (List.map fst params) args in
   CS.Tvar.subst subst ty
 

src/ecDecl.mli

@@ -43,7 +43,7 @@ val tydecl_as_record   : tydecl -> (form * (EcSymbols.symbol * EcTypes.ty) list)
 
 val abs_tydecl : ?tc:Sp.t -> ?params:ty_pctor -> locality -> tydecl
 
-val ty_instanciate : ty_params -> ty list -> ty -> ty
+val ty_instantiate : ty_params -> ty list -> ty -> ty
 
 (* -------------------------------------------------------------------- *)
 type locals = EcIdent.t list

src/ecEnv.ml

@@ -2815,7 +2815,7 @@ module Ax = struct
   let rebind name ax env =
     MC.bind_axiom name ax env
 
-  let instanciate p tys env =
+  let instantiate p tys env =
     match by_path_opt p env with
     | Some ({ ax_spec = f } as ax) ->
         Tvar.f_subst ~freshen:true (List.map fst ax.ax_tparams) tys f

src/ecEnv.mli

@@ -168,7 +168,7 @@ module Ax : sig
   val iter : ?name:qsymbol -> (path -> t -> unit) -> env -> unit
   val all  : ?check:(path -> t -> bool) -> ?name:qsymbol -> env -> (path * t) list
 
-  val instanciate : path -> EcTypes.ty list -> env -> form
+  val instantiate : path -> EcTypes.ty list -> env -> form
 end
 
 (* -------------------------------------------------------------------- *)

src/ecFol.mli

@@ -116,7 +116,7 @@ val f_ty_app : EcEnv.env -> form -> form list -> form
 
 (* -------------------------------------------------------------------- *)
 (* WARNING : this function should be use only in a context ensuring
- * that the quantified variables can be instanciated *)
+ * that the quantified variables can be instantiated *)
 
 val f_betared : form -> form
 

src/ecHiInductive.ml

@@ -132,7 +132,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
       let tdecl = EcEnv.Ty.by_path_opt tname env0
         |> odfl (EcDecl.abs_tydecl ~params:(`Named tparams) lc) in
       let tyinst () =
-        fun ty -> ty_instanciate tdecl.tyd_params targs ty in
+        fun ty -> ty_instantiate tdecl.tyd_params targs ty in
 
       match tdecl.tyd_type with
       | Abstract _ ->

src/ecLowGoal.ml

@@ -168,7 +168,7 @@ module LowApply = struct
     | PTGlobal (p, tys) ->
         (* FIXME: poor API ==> poor error recovery *)
         let env = LDecl.toenv (hyps_of_ckenv tc) in
-        (pt, EcEnv.Ax.instanciate p tys env, subgoals)
+        (pt, EcEnv.Ax.instantiate p tys env, subgoals)
 
     | PTTerm pt ->
       let pt, ax, subgoals = check_ `Elim pt subgoals tc in

src/ecMatching.ml

@@ -915,7 +915,7 @@ let f_match opts hyps (ue, ev) f1 f2 =
       raise MatchFailure;
     let clue =
       try  EcUnify.UniEnv.close ue
-      with EcUnify.UninstanciateUni -> raise MatchFailure
+      with EcUnify.UninstantiateUni -> raise MatchFailure
     in
       (ue, clue, ev)